Verification and Implementation of Dependable Controllers

Author

Sacha, Krzysztof

Author_Institution

Warsaw Univ. of Technol., Warsaw

fYear

2008

fDate

26-28 June 2008

Firstpage

143

Lastpage

151

Abstract

A method is described for modeling, verification and automatic generation of code for PLC controllers. The modeling of requirements and the implementation of code are based on a definition of a finite state time machine. The verification process uses UPPAAL, a model checking tool for the networks of timed automata. A conversion between both models is done automatically. The method starts from modeling the desired behavior of the controller by means of an UML- based state machine diagram, and ends-up with a complete program in one of the IEC 1131 languages.

Keywords

Unified Modeling Language; control engineering computing; finite state machines; program verification; programmable controllers; IEC 1131 languages; PLC controllers; UPPAAL; dependable controllers verification; finite state time machine; model checking tool; timed automata; Automata; Automatic control; Automatic generation control; Automatic programming; Electronic mail; IEC standards; Industrial control; Programmable control; Safety; Unified modeling language; Dependability; PLC controller; automatic code generation; model checking; timed automata;

fLanguage

English

Publisher

ieee

Conference_Titel

Dependability of Computer Systems, 2008. DepCos-RELCOMEX '08. Third International Conference on

Conference_Location

Szklarska Poreba

Print_ISBN

978-0-7695-3179-3

Type

conf

DOI

10.1109/DepCoS-RELCOMEX.2008.30

Filename

4573051