Title :
A complete framework for controller verification in manufacturing
Author :
Gerber, Christian ; Preusse, Sebastian ; Hanisch, Hans-Michael
Author_Institution :
Inst. of Comput. Sci., Autom. Technol., Univ. of Halle-Wittenberg, Halle, Germany
Abstract :
Programmable Logic Controllers (PLCs) have been established as standard devices for automation and process control since the 1990s. Although a lot of research work has been done on the field of controller modeling and verification, it is still daily practice that control software is manually developed without applying formal validation methods. On the other hand, controller modeling is often seen detached from the plant or its model, i.e. as an open loop. The results of analysis of open-loop controller behavior give very little or almost no indications of the correct behavior of the closed-loop system. The contribution therefore proposes an approach to generate formal models out of PLC code. These controller models enable formal verification of the closed loop in combination with a specification. Due to the year of publication, all solution approaches are based on the syntax definition of the IEC 61131-3, which is not fulfilled by every industrial PLC vendor. Therefore, this contribution will show a way to use the defined xml formats of the Technical Committee 6 of the PLCopen as input for the formal model generation.
Keywords :
control system synthesis; formal specification; formal verification; process control; programmable controllers; IEC 61131-3; PLCopen; XML formats; closed loop system; formal model generation; formal validation method; industrial PLC vendor; open loop controller modeling; process control software; programmable logic controller verification; standard devices; syntax definition; technical committee;
Conference_Titel :
Emerging Technologies and Factory Automation (ETFA), 2010 IEEE Conference on
Conference_Location :
Bilbao
Print_ISBN :
978-1-4244-6848-5
DOI :
10.1109/ETFA.2010.5641220