A Formal Design Model for Mechatronic Systems

For successful mechatronic system development, the views of all developers produced should be well integrated into a whole, reducing any risks of inconsistencies and conflicts. The model-based verification techniques use models to describe the possible system behavior in a mathematically precise and unambiguous manner. In particular model checking provides the basis for a whole range of verification techniques ranging from an exhaustive exploration to experiments with a restrictive set of scenarios. Here we propose a framework for verifying mechatronic-design systems based on symbolic model checking. Moreover this framework is an approach based on a novel semantics called p-stable.