FACT is a probabilistic model checker that computes confidence intervals for the evaluated properties of Markov chains with unknown transition probabilities when observations of these transitions are available.
Despite the success of quantitative verification, the usefulness of its results depends on the accuracy of the analysed models. Although model states and transitions are typically easy to identify, transition probabilities and rates need to be estimated. The common practice is to obtain these estimates through model fitting to log data or run-time observations, or from domain experts. In either case, the values used in the analysed models contain estimation errors. These errors are then propagated and may produce imprecise results that can lead to invalid design or verification conclusions. The FACT probabilistic model checker is not affected by this problem. FACT can compute confidence intervals for the properties of a common class of parametric Markov chains for which observations of the transitions associated with the unknown probabilities are available.
The operation of FACT is underpinned by the theoretical results from (Calinescu et al. 2015) and the tool integrates established components that include the PRISM parametric quantitative verification engine, the MATLAB convex programming toolbox YALMIP and a purpose-built hill climbing optimiser. The modular architecture of the tool makes it easy to replace these components with functionally equivalent ones and to extend the tool.
The FACT probabilistic model checker will be presented at TACAS 2016 (Calinescu et al. 2016).
Downloading FACTFACT is freely available under the GNU General Public Licence as a deployable binary here or the full source code may be downloaded here. Please not that the UI utilises JavaFX and as such requires Java 8 in order to compile. Complete instructions on how to install and use FACT for the first time are available on the Getting Started page.
Contacting usIf you wish to contact the authors then please use the following email addresses:
Radu Calinescu: firstname.lastname@example.org
Kenneth Johnson: email@example.com
Colin Paterson: firstname.lastname@example.org
ReferencesR. Calinescu, C. Ghezzi, K. Johnson, M. Pezze, Y. Raq, and G. Tamburrelli (2015). Formal verication with confidence intervals to establish quality of service properties of software systems. IEEE Transactions on Reliability 65(1):107-125, http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=7177126
R. Calinescu, K. Johnson, C. Paterson (2016). FACT: A probabilistic model checker for formal verification with confidence intervals. M. Chechik and J.-F. Raskin (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - TACAS 2016, LNCS 9636, pp. 540–546.