Design and verification of industrial logic controllers with UML and statecharts

Author

Bonfè, Marcello ; Fantuzzi, Cesare

Author_Institution

Dipt. di Ingegneria, Ferrara Univ., Italy

Volume

2

fYear

2003

fDate

23-25 June 2003

Firstpage

1029

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Control Applications, 2003. CCA 2003. Proceedings of 2003 IEEE Conference on

Print_ISBN

0-7803-7729-X

Type

conf

DOI

10.1109/CCA.2003.1223152

Filename

1223152