Skip to Main content Skip to Navigation
Conference papers

Parameterized Specification and Verification of PLC Systems in Coq

Hai Wan 1 Xiaoyu Song 1 Ming Gu 1 
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
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 har- nessed to represent the component specifications. Modular and parameterized specification and verification are proposed. An illustrative example demonstrates the effectiveness of the method.
Document type :
Conference papers
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Hai Wan Connect in order to contact the contributor
Submitted on : Tuesday, March 8, 2011 - 7:00:30 AM
Last modification on : Thursday, February 3, 2022 - 11:16:49 AM
Long-term archiving on: : Thursday, June 9, 2011 - 2:18:54 AM


Files produced by the author(s)


  • HAL Id : inria-00516016, version 1



Hai Wan, Xiaoyu Song, Ming Gu. Parameterized Specification and Verification of PLC Systems in Coq. 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, Aug 2010, Taipei, Taiwan. ⟨inria-00516016⟩



Record views


Files downloads