PV4 FACT: Formal verification with confidence intervalscomputes confidence intervals for given properties of timed automata

Probabilistic model checker that can compute confidence intervals for certain properties for which observations of the transitions associated with unknown probabilities are available.

Application domain/field

Type of tool

Model checker

Expected input

Format:

Expected output

Confidence interval for each confidence level α from the user-specified range

Internals

FACT uses a four-step approach:
  1. Parametric quantitative verification is used to obtain an algebraic expressed for the analysed PCTL property (uses PRISM)
  2. Simultaneous confidence intervals are calculated for each set of parameters
  3. Uses results of step 2 for a convex optimisation problem whose solution represents an α confidence interval for the analysed property
  4. Uses a heuristic to seek alternative confidence intervals. This optimisation might reduce the width of property confidence intervals.

Comments

License: GNU General Public LIcense
Model checking Probabilistic

Links

Project page: http://www-users.cs.york.ac.uk/~cap/FACT

Related papers

https://doi.org/10.1007/978-3-662-49674-9_32 (TACAS '16)

Last publication date

9 April 2016

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.