DocumentCode
2346787
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
fYear
2010
fDate
25-27 Aug. 2010
Firstpage
179
Lastpage
182
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Theoretical Aspects of Software Engineering (TASE), 2010 4th IEEE International Symposium on
Conference_Location
Taipei
Print_ISBN
978-1-4244-7847-7
Type
conf
DOI
10.1109/TASE.2010.12
Filename
5587715
Link To Document