Title :
Design and verification of industrial logic controllers with UML and statecharts
Author :
Bonfè, Marcello ; Fantuzzi, Cesare
Author_Institution :
Dipt. di Ingegneria, Ferrara Univ., Italy
Abstract :
The paper describes a methodological framework that aims to apply formal design and verification techniques to the domain of logic control and supervision for manufacturing systems. The methodology is based on an object-oriented approach, supported by a syntactical and semantical adaptation of the semi-formal software specification languages UML and statecharts. The modeling languages have been subsequently formalized, according to a semantics that take into account the concepts described in the IEC 61131-3 standard for industrial controllers programming, in order to prove correctness properties expressed in the temporal logic CTL. The verification process is performed by means of the model-checking tool SMV.
Keywords :
formal languages; formal verification; industrial control; manufacturing systems; object-oriented methods; specification languages; temporal logic; CTL temporal logic; IEC 61131-3 standard; SMV model checking tool; UML; correctness properties; formal design; industrial controllers programming; industrial logic controller; manufacturing systems; modeling languages; object-oriented approach; statecharts semiformal software; supervision; verification techniques; Control systems; Electrical equipment industry; IEC standards; Industrial control; Logic design; Logic programming; Manufacturing industries; Manufacturing systems; Object oriented modeling; Unified modeling language;
Conference_Titel :
Control Applications, 2003. CCA 2003. Proceedings of 2003 IEEE Conference on
Print_ISBN :
0-7803-7729-X
DOI :
10.1109/CCA.2003.1223152
