VESTA: A Statistical Model-checker and Analyzer for Probabilistic Systems. VESTA is a tool for statistical analysis of probabilistic systems. It supports statistical model-checking [6, 7] and statistical evaluation of expected values of temporal expressions. For model-checking VESTA uses a sequence of inter-related statistical hypothesis testing to check if a property specified in probabilistic computation tree logic (PCTL) [3] or continuous stochastic logic (CSL) is satisfied by a stochastic model. Furthermore, VESTA supports the statistical computation of expected values of expressions written in a query language called Quantitative Temporal Expressions (or QUATEX in short). We next describe the various components of the tool.

References in zbMATH (referenced in 16 articles )

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

  1. Ballarini, Paolo; Duflot, Marie: Applications of an expressive statistical model checking approach to the analysis of genetic circuits (2015)
  2. Belzner, Lenz; De Nicola, Rocco; Vandin, Andrea; Wirsing, Martin: Reasoning (on) service component ensembles in rewriting logic (2014)
  3. Liu, Liya; Hasan, Osman; Aravantinos, Vincent; Tahar, Sofiène: Formal reasoning about classified Markov chains in HOL (2013)
  4. Liu, Liya; Hasan, Osman; Tahar, Sofiène: Formal reasoning about finite-state discrete-time Markov chains in HOL (2013)
  5. Bae, Kyungmin; Ölveczky, Peter Csaba; Feng, Thomas Huining; Lee, Edward A.; Tripakis, Stavros: Verifying hierarchical Ptolemy II discrete-event models using real-time maude (2012)
  6. Barbot, Beno{^i}t; Haddad, Serge; Picaronny, Claudine: Coupling and importance sampling for statistical model checking (2012)
  7. Bruni, Roberto; Corradini, Andrea; Gadducci, Fabio; Lluch Lafuente, Alberto; Vandin, Andrea: Modelling and analyzing adaptive self-assembly strategies with Maude (2012)
  8. Meseguer, José: Twenty years of rewriting logic (2012)
  9. AlTurki, Musab; Meseguer, José: PVeSTA: A parallel statistical model checking and quantitative analysis tool (2011)
  10. Hasan, Osman; Tahar, Sofiène: Reasoning about conditional probabilities in a higher-order-logic theorem prover (2011)
  11. Liu, Liya; Hasan, Osman; Tahar, Sofiène: Formalization of finite-state discrete-time Markov chains in HOL (2011)
  12. Alturki, Musab; Meseguer, José; Gunter, Carl A.: Probabilistic modeling and analysis of dos protection for the ASV protocol (2009)
  13. Hasan, Osman; Tahar, Sofiène: Probabilistic analysis of wireless systems using theorem proving (2009)
  14. Ölveczky, Peter Csaba; Thorvaldsen, Stian: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude (2009)
  15. Hasan, Osman; Tahar, Sofiène: Using theorem proving to verify expectation and variance for discrete random variables (2008)
  16. Greifeneder, Jürgen: Formal analysis of the time behaviour of network-based automation systems. (2007)