Automatic Generation of Simulation Scenarios for Statistical Model Checking of Real-Time Systems


Toni Mancini, Enrico Tronci
Sapienza Università di Roma

Titolo della presentazione

Automatic Generation of Simulation Scenarios for Statistical Model Checking of Real-Time Systems

Autori

Toni Mancini
Sapienza Università di Roma
Enrico Tronci
Sapienza Università di Roma

Tipologia della presentazione

Presentazione tecnica

Abstract

Synchronous modelling languages (e.g., Modelica, Simulink) assume that the execution of a software function takes no time and the time allowed for its computation (e.g., within a sampling-and-holding schema) is explicitly constrained within the model. This enables a separation-of-concerns approach where the correctness of timing wrt the dynamics of the physical system can be verified through simulation and, separately, we can then check that the Worst-Case Execution Time (WCET) of the code implementation is indeed less than or equal to the timing allowed for that computation within our simulation model. It is well known that Montecarlo-based simulation and statistical model checking techniques can be used to verify, with any given statistical confidence, the correctness of the time constraints for the software functions in our simulation model. However, effectively generating simulation scenarios (i.e., sequences of exogenous events) that satisfy environment constraints (to avoid testing our systems on never-occurring scenarios) is a hard problem. Ignoring such constraints may lead to overprovisioning, and thus increase the cost of the overall system. We present an efficient algorithm to automatically generate simulation scenarios satisfying given constraints defined through finite-state automata.


Ulteriore materiale

  • Slide della presentazione: [pdf]

Per ulteriori dettagli su questa presentazione, cliccare sul pulsante seguente: