Formalization and Verification of PLC Timers in Coq

Hai Wan 1 Gang Chen 2 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) are widely used in embedded systems. A timer plays a pivotal role in PLC real-time applications. The paper presents a formalization of TON-timers of PLC programs in the theorem proving system Coq. The behavior of a timer is characterized by a set of axioms at an abstract level. PLC programs with timers are modeled in Coq. As a case study, the quiz machine problem with timer is investigated. Relevant timing properties of practical interests are proposed and proven in Coq. This work unveils the hardness of timer modeling in embedded systems. It is an attempt of formally proving the correctness of PLC programs with timer control.
Type de document :
Communication dans un congrès
33rd Annual IEEE International Computer Software and Applications Conference, Jul 2009, Seattle,Washington, United States. 2009
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00516011
Contributeur : Hai Wan <>
Soumis le : mardi 8 mars 2011 - 07:00:10
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29
Document(s) archivé(s) le : samedi 3 décembre 2016 - 00:35:55

Fichier

REG-278-WAN.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00516011, version 1

Collections

Citation

Hai Wan, Gang Chen, Xiaoyu Song, Ming Gu. Formalization and Verification of PLC Timers in Coq. 33rd Annual IEEE International Computer Software and Applications Conference, Jul 2009, Seattle,Washington, United States. 2009. 〈inria-00516011〉

Partager

Métriques

Consultations de la notice

273

Téléchargements de fichiers

369