Towards Model Checking of Simulation Models for Embedded System Development

Modeling and simulation has been widely used to develop embedded systems and cyber-physical systems, especially in safety-critical domains. While models for such systems are required to be rigidly verified, simulation offers only partial observations on them with a limited number of test cases. Model checking techniques of timed automata would not be directly applied to formal verification of simulation models due to the differences in execution semantics and model composition. In order to enable model checking of simulation models, this paper presents an algorithm to obtain region transition systems from models written in an M&S formalism. Such region transition systems could be exhaustively checked by the model checking techniques without any modification.