Skip to Main content Skip to Navigation
Conference papers

The Verification of PLC Program Based on Interactive Theorem Proving Tool COQ

Litian Xiao 1 Ming Gu 2 Jiaguang Sun 3 
2 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : COQ is an interactive theorem proving tool. The paper abstractly describes the feature of COQ, the architecture and working modes of PLC program with the example of typical PLC. It also introduces the first-order logic syntax and semantics of Intuitionistic Logic. It briefly introduces the main Gallina language syntax elements, the corresponding use methods and main theorem proving tactic on COQ. The work has modeled kernel data type and basic statements and and the denotational semantics of PLC program with Gallina. It has given the correctness proof of PLC program based on theorem proving, i.e. based on semantics function the relationship of configuration between the before codes execution and the after is proved. The main purpose is to prove whether a PLC program satisfies certain nature within a scan period.
Document type :
Conference papers
Complete list of metadata
Contributor : Hehua Zhang Connect in order to contact the contributor
Submitted on : Friday, July 29, 2011 - 5:07:04 AM
Last modification on : Thursday, February 3, 2022 - 11:15:54 AM


  • HAL Id : inria-00612408, version 1



Litian Xiao, Ming Gu, Jiaguang Sun. The Verification of PLC Program Based on Interactive Theorem Proving Tool COQ. 4th IEEE International Conference on Computer Science and Information Technology(ICCSIT2011), Jun 2011, Chengdu, China. ⟨inria-00612408⟩



Record views