Title :
Verification and Implementation of Dependable Controllers
Author :
Sacha, Krzysztof
Author_Institution :
Warsaw Univ. of Technol., Warsaw
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;
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
DOI :
10.1109/DepCoS-RELCOMEX.2008.30
