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

https://hal.inria.fr/inria-00516016
Contributor : Hai Wan <>
Submitted on : Tuesday, March 8, 2011 - 7:00:30 AM
Last modification on : Monday, December 14, 2020 - 3:30:22 PM
Long-term archiving on: : Thursday, June 9, 2011 - 2:18:54 AM

File

Modular_and_Parameterized_veri...
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00516016, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

500

Files downloads

516