Paper Info
Title
PRISM 4.0: verification of probabilistic real-time systems
Abstract
This paper describes a major new release of the PRISMprobabilistic 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.
Year
DOI
Venue
2011
10.1007/978-3-642-22110-1_47
CAV
Keywords
Field
DocType
application domain,model system,probabilistic model,new component,explicit-state probabilistic model checking,benchmark suite,avionic system,prismprobabilistic model checker,probabilistic real-time system,major new release,statistical model checking
Model checking,Cryptographic protocol,Nondeterministic algorithm,Computer science,Automaton,Avionics,PRISM model checker,Real-time computing,Theoretical computer science,Probabilistic logic,Bluetooth,Distributed computing
Conference
Citations 
PageRank 
References 
801
23.09
13
Authors
3
Search Limit
100801
Name
Order
Citations
PageRank
Marta Z. Kwiatkowska16118322.21
Gethin Norman24163193.68
David Parker34018184.00