|
[KNP07a]
Marta Kwiatkowska, Gethin Norman and David Parker.
Stochastic Model Checking.
In M. Bernardo and J. Hillston (editors), Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of Lecture Notes in Computer Science (Tutorial Volume), pages 220-270, Springer.
June 2007.
[pdf]
[bib]
[Tutorial paper covering probabilistic model checking of DTMCs/CTMCs and PRISM.]
|
|
Downloads:
 pdf (1.01 MB)
 bib
|
|
Notes:
Note that the online copy of this paper contains some minor fixes, compared to the published version.
The original publication is available at link.springer.com.
|
|
Links:
[Google]
[Google Scholar]
|
Abstract.
This tutorial presents an overview of model checking for
both discrete and continuous-time Markov chains (DTMCs and CTMCs).
Model checking algorithms are given for verifying DTMCs and CTMCs
against specifications written in probabilistic extensions of
temporal logic, including quantitative properties with rewards.
Example properties include the probability that a fault occurs and
the expected number of faults in a given time period.
We also describe the practical application of stochastic model
checking with the probabilistic model checker PRISM by outlining the
main features supported by PRISM and three real-world case studies:
a probabilistic security protocol, dynamic power management and a
biological pathway.
|