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 Condit...

Full description

Saved in:
Bibliographic Details
Main Authors: Patil, S., Vyatkin, V., Sorouri, M.
Format: Conference Proceeding
Language:English
Subjects:
Closed-Loop Modeling
Formal Verification
NCES
SESA
ViVe
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1946-0740
1946-0759
DOI:10.1109/ETFA.2012.6489678