Distributed Statistical Model Checking for Discrete Event Simulators
A property in the simulator-independent query language of MultiVeStA, and the obtained plot.
MultiVeStA is an efficient statistical analysis tool which can be easily integrated with existing discrete event simulators, enriching them with distributed Statistical Analysis and Statistical Model Checking capabilities.
The tool originally focused on transient-time analysis, but it has recently been enriched also with steady-state (or long-run) analysis capabilities. Please check here for further details on the latter.
Supported Simulators (in alphabetic order):
- Alchemist: a simulator targeting chemical-oriented computational systems
- ARGoS: a multi-robot, multi-engine simulator for heterogeneous Swarm robotics
- Bike Sharing Simulator — TopoChecker topological model checker: A Tool-chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems
- Bio-PEPA: a language for the modelling and the analysis of biochemical networks
- CO2: A Contract-Oriented middleware
- DESMO-J: a framework for discrete-event modeling and simulation (contributor Claudia Cauli)
- DEUS: a general-purpose, open-source, simulator for the analysis of large scale systems
- Edinburgh Bus Simulator: a tool for the analysis of public transportation systems
- ERODE: Evaluation and Reduction of Ordinary Differential Equations
- QFLan: a probabilistic feature-oriented language with quantitative constraints for product families
- MISSCEL: an interpreter and simulator for the Service Component Ensemble Language
- ONE: the Opportunistic Network Environment discrete event simulator (details on integration and contributors are provided here)
- OnPlan: a framework for simulation-based online planning
- Probabilistic Maude: an engine to execute probabilistic rewrite theories. Try out MultiVeStA with an implementation of a dice in PMaude
- Any Python simulator, using Py4J
- A built in DTMC and CTMC engine
- other simulators coming soon
- …and yours with just few lines of code (just contact us!).
Our papers on MultiVeStA
- MultiVeStA: Statistical Model Checking for Discrete Event Simulators, Stefano Sebastio, Andrea Vandin, VALUETOOLS’13 (please cite this work) (extended version)
- Transient and Steady-State Statistical Analysis for Discrete Event Simulators, Stephen Gilmore, Daniel Reijsbergen, Andrea Vandin, IFM’17;
- A Tool-chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems, Vincenzo Ciancia, Diego Latella, Mieke Massink, Rytis Paskauskas, Andrea Vandin, ISOLA’16
- Statistical Model Checking for Product Lines, Maurice ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin, ISOLA’16
- Statistical Analysis of Probabilistic Models of Software Product Lines with Quantitative Constraints, Maurice ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin SPLC’15
- Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking, Maurice ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin, FMSPLE’15
- An Analysis Pathway for the Quantitative Evaluation of Public Transport Systems, Stephen Gilmore, Mirco Tribastone, Andrea Vandin, IFM’14
- Distributed statistical analysis of complex systems modeled through a chemical metaphor, Danilo Pianini, Stefano Sebastio, Andrea Vandin, HPCS’14;
- Reasoning (on) Service Component Ensembles in Rewriting Logic, Lenz Belzner, Rocco De Nicola, Andrea Vandin, Martin Wirsing, SAS’14
- A Computational Field Framework for Collaborative Task Execution in Volunteer Clouds, Stefano Sebastio, Michele Amoretti, Alberto Lluch-Lafuente, SEAMS’14
- Reputation-based Cooperation in the Clouds, Alessandro Celestini, Alberto Lluch-Lafuente, Philip Mayer, Stefano Sebastio, Francesco Tiezzi, IFIPTM’14
- AVoCloudy: a simulator of volunteer clouds, Stefano Sebastio, Michele Amoretti, Alberto Lluch-Lafuente, Software: Practice and Experience
- A Workload-Based Approach to Partition the Volunteer Cloud, Stefano Sebastio, Antonio Scala, IEEE CIC’15
Papers by OTHERS using MultiVeStA
- Statistical Model Checking of Opportunistic Network Protocols, Shiraj Arora, Ankit Rathor, M. V. Panduranga Rao, AINTEC’15
- A Contract-oriented middleware, Massimo Bartoletti, Tiziana Cimoli, Maurizio Murgia, Alessandro Sebastian Podda, Livio Pompianu, FACS’15
- OnPlan: A Framework for Simulation-Based Online Planning, Lenz Belzner, Rolf Hennicker, Martin Wirsing, FACS’15
Other related papers
- VESTA: A Statistical Model-checker and Analyzer for Probabilistic Systems
- PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool
- PMaude: Rewrite-based Specification Language for Probabilistic Object Systems
We are grateful to the proposers of (P)VeStA, our starting point: Gul Agha, Musab Alturki, José Meseguer, Koushik Sen and Mahesh Viswanathan.
Furthermore, we thank the main author of Alchemist (Danilo Pianini), who provided valuable help and suggestions to improve MultiVeStA, as well as Benjamin Byholm, who helped us in extending the support of MultiVeStA to python simulators. We also thank Stephen Gilmore and Mirco Tribastone, for their help in integrating MultiVeStA with BioPEPA.
Last but not least, we thank Michele Amoretti and Alberto Lluch Lafuente, who supported and suggested this work from the very beginning.
For suggestions, remarks, bugs, or to have more information about the usage of MultiVeStA, or about its integration with a simulator, please do not hesitate to contact: