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 is maintained and developed by Stefano Sebastio and Andrea Vandin. The tool comes as an extension of the existing VeStA and PVeStA tools, developed at the Department of Computer Science at the University of Illinois at Urbana-Champaign.
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, resorting to 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 (please cite this work) in the proceedings of VALUETOOLS’13 (extended version)
- A Tool-chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems, Vincenzo Ciancia, Diego Latella, Mieke Massink, Rytis Paskauskas, Andrea Vandin, in the proceedings of (ISOLA’16);
- Statistical Model Checking for Product Lines, Maurice ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin, in the proceedings of (ISOLA’16);
- Statistical Analysis of Probabilistic Models of Software Product Lines with Quantitative Constraints in the proceedings of SPLC’15
- Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking in the proceedings of FMSPLE’15
- An Analysis Pathway for the Quantitative Evaluation of Public Transport Systems in the proceedings of IFM’14
- Distributed statistical analysis of complex systems modeled through a chemical metaphor in the proceedings of HPCS’14
- Reasoning (on) Service Component Ensembles in Rewriting Logic in the proceedings of SAS’14
- A Computational Field Framework for Collaborative Task Execution in Volunteer Clouds in the proceedings of SEAMS’14
- Reputation-based Cooperation in the Clouds in the proceedings of IFIPTM’14
- AVoCloudy: a simulator of volunteer clouds in Software: Practice and Experience
- A Workload-Based Approach to Partition the Volunteer Cloud in the proceedings of IEEE CIC’15
Papers by OTHERS using MultiVeStA
- Statistical Model Checking of Opportunistic Network Protocols in the proceedings of AINTEC’15
- A Contract-oriented middleware, in the proceedings of FACS’15
- OnPlan: A Framework for Simulation-Based Online Planning, in the proceedings of 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: