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.
For more details on this presentation please click the button below: