TY - GEN

T1 - PVeStA

T2 - 4th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2011

AU - AlTurki, Musab

AU - Meseguer, José

PY - 2011/9/26

Y1 - 2011/9/26

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.

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.

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

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

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

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

M3 - Conference contribution

AN - SCOPUS:80053033779

SN - 9783642229435

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 386

EP - 392

BT - Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Proceedings

Y2 - 30 August 2011 through 2 September 2011

ER -