The FACT Confidence Interval Synthesiser is a Java command-line tool that establishes confidence intervals for PCTL-formalised QoS properties of software and embedded systems, starting from the algebraic expression of these properties. The tool automates the second stage of the FACT approach.
The FACT tool requires the following software tools and libraries:
The FACT toolchain takes as input
To illustrate the usage of the FACT toolchain, we consider the following
parametric Markov chain model of a web-server handling HTTP requests.
- Download the PMC model here: httprequests.pm
- Download the PCTL properties file here: properties.pctl
The parametric model checking of the first PCTL formulae yields the algebraic expression (-160*w1*y2*x1-160*w1*y2*x2+77*k1*z1*y1+160*y2*x1-77*z1*y1-77*z2*y1+160*w1*y2+160*y1)/160. Using this expression and state transition observations, we form the FACT input file:
(-160*w1*y2*x1-160*w1*y2*x2+77*k1*z1*y1+160*y2*x1-77*z1*y1-77*z2*y1+160*w1*y2+160*y1)/160
0.85 0.99 0.01
x 3 5963
3414
2
2547
y 3 10000
4037
5963
0
z 3 1560
407
2
1151
k 2 407
407
0
w 2 2547
2546
1
END
This input file specifies a FACT experiment in which the algebraic expression P given in the first line of the record is analysed with confidence levels between 85% - 99% with a step of 1%, as specified in the second line of the file.
Line 3 comprises the parameter name prefix 'x', the number 3 that signifies there are three parameters x1, x2 and x3; and an integer representing the total number of observations made for these parameters, which in our example is 5963.
The subsequent three lines each contain a number that specify how many times the system was observed taking that transitions associated with the transition probabilities x1, x2 and x3. In our example, the transition x1 was observed 3414 times, x2 observed 2 times and x3 observed 2547. The sum of these values gives the number of observations, 5963. Similar information is provided for parameters y, z, k and w from the algebraic expression P.
The FACT tool synthesises and outputs a confidence interval for the property in the format:
0.85, 0.994323585712125, 0.9999972018176742, 51, 143.239
0.86, 0.9941436356413703, 0.9999972017607284, 51, 284.09
0.87, 0.9939485660174432, 0.9999972017035086, 51, 427.288
0.88, 0.9937633043667259, 0.9999998600072693, 51, 568.768
0.89, 0.9935019178756483, 0.9999972015852509, 51, 712.38
0.9, 0.9932426939822329, 0.9999972015216917, 51, 856.301
0.91, 0.9929523386533454, 0.9999972014590576, 51, 1000.696
0.92, 0.99262295656729, 0.9999972013946028, 51, 1150.168
0.93, 0.9922433210069956, 0.9999972013267711, 51, 1299.359
0.9400000000000001, 0.9917967327355913, 0.9999998600068309, 51,
1442.913
0.9500000000000001, 0.9912568397866651, 0.9999972011784632, 51,
1597.501
0.9600000000000001, 0.990581676153592, 0.9999972011350197, 51,
1746.481
0.9700000000000001, 0.9896745477096927, 0.9999998600028888, 51,
1900.782
0.9800000000000001, 0.988345715665172, 0.9999998600025128, 51,
2049.781
0.9900000000000001, 0.9859600879864435, 0.9999994400392352, 51,
2200.52
The first number represents the degree of confidence, the next two numbers specify the bounds of the confidence interval, the second last number counts the hill-climbing iterations and the last number records the cumulative analysis time.