Coupling simulation and model checking to examine selected mechanical constraints of automated production systems

Modeling complex mechatronic systems containing parts such as mechanics, electronics and software is a major challenge for the engineering of automation production systems. As a result, many modeling languages as well as tools (e.g. petri nets or MATLAB/Simulink) and verification approaches (e.g. testing, simulation or formal verification) that focus on special challenges to model the mechatronic system correctly have already been developed. However, a holistic approach combining the strengths of the individual approaches adapted for the engineering of automation production systems has not yet been developed. In this paper we consider the combination of simulation with MATLAB/Simulink and a discrete event simulation model allowing model checking of specific constraints. Hence, the strengths of both approaches' formal verification, i.e. to identify not only faults but also correctness of a system, and simulation, i.e. showing the exact time behavior of the system, can be combined. A key challenge of our approach is to identify an appropriate level of abstraction of both models. The evaluation of the presented approach is introduced by modeling the throughput of a simple automation production system.