Fabian Vu, Michael Leuschel, Atif Mashkoor,
"Validation of Formal Models by Timed Probabilistic Simulation"
, in Alexander Raschke and Dominique Mèry: Rigorous State-Based Methods - 8th International Conference, ABZ 2021, Ulm, Germany, June 9-11, 2021, Proceedings, Serie Lecture Notes in Computer Science, Vol. 12709, Springer, Seite(n) 81-96, 2021
Original Titel:
Validation of Formal Models by Timed Probabilistic Simulation
Sprache des Titels:
Englisch
Original Buchtitel:
Rigorous State-Based Methods - 8th International Conference, ABZ 2021, Ulm, Germany, June 9-11, 2021, Proceedings
Original Kurzfassung:
The validation of a formal model consists of checking its conformance with actual requirements. In the context of (Event-) B, some temporal aspects can typically be validated by LTL or CTL model checking, while other properties can be validated via interactive animation or trace replay. In this paper, we present a new simulation-based validation technique for (Event-) B models called SimB. The proposed technique uses annotations to construct simulations, taking probabilistic and real-time aspects of the models into account. In this fashion, statistical properties of a single simulation run or a series of runs can be checked (e.g., Monte Carlo estimation or hypothesis tests). SimB complements animation and model checking, and its usability has been assessed via several case studies.
Forschungs-