Validation of Formal Models by Timed Probabilistic Simulation

Autor:	Michael Leuschel, Fabian Vu, Atif Mashkoor
Rok vydání:	2021
Předmět:	Model checking business.industry Event (computing) Computer science Probabilistic logic Usability Context (language use) Animation computer.software_genre Data mining business computer Statistical hypothesis testing TRACE (psycholinguistics)
Zdroj:	Rigorous State-Based Methods ISBN: 9783030775421 ABZ
DOI:	10.1007/978-3-030-77543-8_6
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::2fd5103afce43a954f93808978eaee63 https://doi.org/10.1007/978-3-030-77543-8_6 Zobrazit plný text záznamu