PVeStA

PVeStA: A parallel statistical model checking and quantitative analysis tool. 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.


References in zbMATH (referenced in 18 articles )

Showing results 1 to 18 of 18.
Sorted by year (citations)

  1. Durán, Francisco; Rocha, Camilo; Salaün, Gwen: Resource provisioning strategies for BPMN processes: specification and analysis using Maude (2021)
  2. Liu, Si; Ölveczky, Peter Csaba; Wang, Qi; Gupta, Indranil; Meseguer, José: Read atomic transactions with prevention of lost updates: ROLA and its formal analysis (2019)
  3. Lemos, Marcilio O. O.; Dantas, Yuri Gil; Fonseca, Iguatemi E.; Nigam, Vivek: On the accuracy of formal verification of selective defenses for TDoS attacks (2018)
  4. Avni, Guy; Goel, Shubham; Henzinger, Thomas A.; Rodriguez-Navas, Guillermo: Computing scores of forwarding schemes in switched networks with probabilistic faults (2017)
  5. Ölveczky, Peter Csaba: Designing reliable distributed systems. A formal methods approach based on executable modeling in Maude (2017)
  6. Liu, Si; Ölveczky, Peter Csaba; Meseguer, José: Modeling and analyzing mobile ad hoc networks in Real-Time Maude (2016)
  7. Johnsen, Einar Broch; Schlatte, Rudolf; Tapia Tarifa, S. Lizeth: Integrating deployment architectures and resource consumption in timed object-oriented models (2015)
  8. Belzner, Lenz; De Nicola, Rocco; Vandin, Andrea; Wirsing, Martin: Reasoning (on) service component ensembles in rewriting logic (2014) ioport
  9. Grov, Jon; Ölveczky, Peter Csaba: Formal modeling and analysis of google’s megastore in real-time maude (2014) ioport
  10. Bentea, Lucian; Ölveczky, Peter Csaba: A probabilistic strategy language for probabilistic rewrite theories and its application to cloud computing (2013)
  11. Eckhardt, Jonas; Mühlbauer, Tobias; Meseguer, José; Wirsing, Martin: Statistical model checking for composite actor systems (2013)
  12. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2013)
  13. Bruni, Roberto; Corradini, Andrea; Gadducci, Fabio; Lluch Lafuente, Alberto; Vandin, Andrea: Modelling and analyzing adaptive self-assembly strategies with Maude (2012) ioport
  14. Katelman, Michael; Keller, Sean; Meseguer, José: Rewriting semantics of production rule sets (2012)
  15. Meseguer, José: Twenty years of rewriting logic (2012)
  16. Wirsing, Martin; Eckhardt, Jonas; Mühlbauer, Tobias; Meseguer, José: Design and analysis of cloud-based architectures with KLAIM and Maude (2012) ioport
  17. AlTurki, Musab; Meseguer, José: PVeSTA: A parallel statistical model checking and quantitative analysis tool (2011) ioport
  18. Bentea, Lucian; Ölveczky, Peter Csaba: Probabilistic real-time rewrite theories and their expressive power (2011)