Title :
Parameterized Specification and Verification of PLC Systems in Coq
Author :
Wan, Hai ; Song, Xiaoyu ; Gu, Ming
Author_Institution :
D.CST, Tsinghua Univ., Beijing, China
Abstract :
Programmable logic controllers (PLCs) represent a typical class of embedded software systems. They are widely used in safety-critical industrial applications, such as railways, automotive applications, etc. The paper presents a novel method to specify and verify PLC software systems with the theorem proving system Coq. Dependent inductive data types are harnessed to represent the component specifications. Modular and parameterized specification and verification are proposed. An illustrative example demonstrates the effectiveness of the method.
Keywords :
embedded systems; formal specification; programmable controllers; safety-critical software; systems analysis; Coq; PLC; component specification; embedded software system; modular specification; parameterized specification; parameterized verification; programmable logic controller; safety-critical industrial application; theorem proving system; Compounds; Conferences; Construction industry; Generators; Libraries; Programming; Software;
Conference_Titel :
Theoretical Aspects of Software Engineering (TASE), 2010 4th IEEE International Symposium on
Conference_Location :
Taipei
Print_ISBN :
978-1-4244-7847-7
DOI :
10.1109/TASE.2010.12
