Formal verification of Intelligent Mechatronic Systems with decentralized control logic

This paper introduces an approach to automatic verification of mechatronic systems designed as plug-and-play of Intelligent Mechatronic Components (IMC). The control logic of the system is composed from autonomous controllers of the IMCs and is automatically verified using model-checking. Net Condition Event Systems formalism (a modular extension of Petri net) is used to model the decentralized control logic and discrete-state dynamics of the plant. A re-configurable pick and place robot is used as an illustrative example. At first a three cylinder pick and place robot is used to design our new master-slave architecture for controller design and then the NCES models are re-used without much modification in a new 6 cylinder pick and place robot. The control model is then subjected to model checking using the ViVe/SESA model checker. A multi closed loop model of Plant and Controller is used and controller is extensively verified for safety, liveliness and functional properties of the robot. Computational Tree Logic (CTL) is used to specify these properties.