PRISM 4.0: Verification of probabilistic real-time systems

Journal article

This paper describes a major new release of the PRISM probabilistic model checker, adding, in particular, quantitative verification of (priced) probabilistic timed automata. These model systems exhibiting probabilistic, nondeterministic and real-time characteristics. In many application domains, all three aspects are essential; this includes, for example, embedded controllers in automotive or avionic systems, wireless communication protocols such as Bluetooth or Zigbee, and randomised security protocols. PRISM, which is open-source, also contains several new components that are of independent use. These include: an extensible toolkit for building, verifying and refining abstractions of probabilistic models; an explicit-state probabilistic model checking library; a discrete-event simulation engine for statistical model checking; support for generation of optimal adversaries/strategies; and a benchmark suite. © 2011 Springer-Verlag.

Authors: Kwiatkowska, M; Norman, G; Parker, D

• Journal: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
• Volume: 6806 LNCS
• Pages: 585-591
• Publication date: 2011-01-01
• DOI: 10.1007/978-3-642-22110-1_47
• EISSN: 1611-3349
• ISSN: 0302-9743
• Language: English