Abstract
We extend the model checking tool MultiVeStA with statistical model checking of steady-state properties. Since MultiVeStA acts as a front-end for simulation tools, it confers this ability onto any tool with which it is integrated. The underlying simulation models are treated as black-box systems. We will use an approach based on batch means using the ASAP3 algorithm. We motivate the work using two case studies: a biochemical model written in the Bio-PEPA language and an application from transport logistics.
Original language | English |
---|---|
Title of host publication | Integrated Formal Methods - 13th International Conference, IFM 2017, Proceedings |
Volume | 10510 LNCS |
Publisher | Springer Verlag |
Publication date | 2017 |
Pages | 145-160 |
ISBN (Print) | 9783319668444 |
DOIs | |
Publication status | Published - 2017 |
Externally published | Yes |
Event | 13th International Conference on Integrated Formal Methods - Turin, Italy Duration: 20 Sept 2017 → 22 Sept 2017 Conference number: 13 |
Conference
Conference | 13th International Conference on Integrated Formal Methods |
---|---|
Number | 13 |
Country/Territory | Italy |
City | Turin |
Period | 20/09/2017 → 22/09/2017 |
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 10510 LNCS |
ISSN | 0302-9743 |
Keywords
- Batch means
- MultiVeStA
- Statistical model checking
- Steady-state