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

Litian Xiao Ming Gu 1 Jiaguang Sun 2
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 : 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.
Type de document :
Communication dans un congrès
4th IEEE International Conference on Computer Science and Information Technology(ICCSIT2011), Jun 2011, Chengdu, China. 2011
Liste complète des métadonnées

https://hal.inria.fr/inria-00612408
Contributeur : Hehua Zhang <>
Soumis le : vendredi 29 juillet 2011 - 05:07:04
Dernière modification le : mardi 17 avril 2018 - 11:24:03

Identifiants

  • HAL Id : inria-00612408, version 1

Collections

Citation

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. 2011. 〈inria-00612408〉

Partager

Métriques

Consultations de la notice

246