TY - CHAP

T1 - PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool

AU - AlTurki, Musab

AU - Meseguer, José

N1 - KAUST Repository Item: Exported on 2020-10-01
Acknowledgements: We thank Koushik Sen, Mahesh Viswanathan, and GulAgha for the original work onVeStA, and Gul Agha and Koushik Sen for theirwork on PMaude andQuaTEx, which provide the basis on whichPVeStAhas been built. This work has been partially supported by NSF grants CNS 08-34709, CNS 07-16638, and CCF 09-05584, King Fahd University of Petroleumand Minerals, and King Abdullah University of Science and Technology.
This publication acknowledges KAUST support, but has no KAUST affiliated authors.

PY - 2011

Y1 - 2011

N2 - Statistical model checking is an attractive formal analysis method for probabilistic systems such as, for example, cyber-physical systems which are often probabilistic in nature. This paper is about drastically increasing the scalability of statistical model checking, and making such scalability of analysis available to tools like Maude, where probabilistic systems can be specified at a high level as probabilistic rewrite theories. It presents PVeStA, an extension and parallelization of the VeStA statistical model checking tool [10]. PVeStA supports statistical model checking of probabilistic real-time systems specified as either: (i) discrete or continuous Markov Chains; or (ii) probabilistic rewrite theories in Maude. Furthermore, the properties that it can model check can be expressed in either: (i) PCTL/CSL, or (ii) the QuaTEx quantitative temporal logic. As our experiments show, the performance gains obtained from parallelization can be very high. © 2011 Springer-Verlag.

AB - Statistical model checking is an attractive formal analysis method for probabilistic systems such as, for example, cyber-physical systems which are often probabilistic in nature. This paper is about drastically increasing the scalability of statistical model checking, and making such scalability of analysis available to tools like Maude, where probabilistic systems can be specified at a high level as probabilistic rewrite theories. It presents PVeStA, an extension and parallelization of the VeStA statistical model checking tool [10]. PVeStA supports statistical model checking of probabilistic real-time systems specified as either: (i) discrete or continuous Markov Chains; or (ii) probabilistic rewrite theories in Maude. Furthermore, the properties that it can model check can be expressed in either: (i) PCTL/CSL, or (ii) the QuaTEx quantitative temporal logic. As our experiments show, the performance gains obtained from parallelization can be very high. © 2011 Springer-Verlag.

UR - http://hdl.handle.net/10754/599416

UR - http://link.springer.com/10.1007/978-3-642-22944-2_28

UR - http://www.scopus.com/inward/record.url?scp=80053033779&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-22944-2_28

DO - 10.1007/978-3-642-22944-2_28

M3 - Chapter

SN - 9783642229435

SP - 386

EP - 392

BT - Algebra and Coalgebra in Computer Science

PB - Springer Nature

ER -