PVeStA: A parallel statistical model checking and quantitative analysis tool

Musab AlTurki, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationAlgebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Proceedings
Pages386-392
Number of pages7
DOIs
StatePublished - Sep 26 2011
Event4th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2011 - Winchester, United Kingdom
Duration: Aug 30 2011Sep 2 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6859 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2011
CountryUnited Kingdom
CityWinchester
Period8/30/119/2/11

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'PVeStA: A parallel statistical model checking and quantitative analysis tool'. Together they form a unique fingerprint.

Cite this