Basile D., Ter Beek M. H., Di Giandomenico F., Fantechi A., Gnesi S., Spagnolo G. O.
Stochastic model-based analysis Möbius Statistical Model Checking Railways Stochastic Hybrid Automata Uppaal SMC Cyber-Physical Systems Stochastic Activity Networks Tool comparison Quantitative analysis
We provide a brief comparison of the modelling and analysis capabilities of two different formalisms and their associated simulation-based tools, acquired from experimenting with these methods and tools on one specific case study. The case study is a cyber-physical system from an industrial railway project, namely a railroad switch heater, and the quantitative properties concern energy consumption and reliability. We modelled and analysed the case study with stochastic activity networks and Möbius on the one hand and with stochastic hybrid automata and Uppaal SMC on the other hand. We give an overview of the performed experiments and highlight specific features of the two methodologies. This yields some pointers for future research and improvements.
Source: ISoLA 2020 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, pp. 368–384, Rhodes, Greece, 20-30/10/2020
Publisher: Springer, Berlin, DEU
@inproceedings{oai:it.cnr:prodotti:434871, title = {30 years of simulation-based quantitative analysis tools: a comparison experiment between Möbius and Uppaal SMC}, author = {Basile D. and Ter Beek M. H. and Di Giandomenico F. and Fantechi A. and Gnesi S. and Spagnolo G. O.}, publisher = {Springer, Berlin, DEU}, doi = {10.1007/978-3-030-61362-4_21}, booktitle = {ISoLA 2020 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, pp. 368–384, Rhodes, Greece, 20-30/10/2020}, year = {2020} }
Basile, Davide
0000-0002-7196-6609
Di Giandomenico, Felicita
0000-0002-8760-7299
Fantechi, Alessandro
0000-0002-4648-4667
Gnesi, Stefania
0000-0002-0139-0421
Spagnolo, Giorgio Oronzo
0000-0002-7771-0882
Ter Beek, Maurice Henri
0000-0002-2930-6367
Formal Methods and Tools (2002-ongoing)
Software Engineering & Dependable Computing (2012-ongoing)
System and Software Evaluation (2002-ongoing)