Formalisation and verification of programmable logic controllers timers in Coq

Hai Wan 1 Chen Gang 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. Timers play a pivotal role in PLC real-time applications. The formalization of timers is of great importance. The study presents a formalization of PLC timers in the theorem proving system Coq, in which the behaviors of timers are characterized by a set of axioms at an abstract level. The authors discuss how to model timers at a proper and sound abstract level. PLC programs with timers are modeled. As a case study, a quiz machine problem with a timer is investigated. This work demonstrates the complexity of formal timer modeling
Type de document :
Article dans une revue
IET Software, Institution of Engineering and Technology, 2011
Liste complète des métadonnées

https://hal.inria.fr/inria-00612410
Contributeur : Hehua Zhang <>
Soumis le : vendredi 29 juillet 2011 - 05:42:12
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Identifiants

  • HAL Id : inria-00612410, version 1

Collections

Citation

Hai Wan, Chen Gang, Xiaoyu Song, Ming Gu. Formalisation and verification of programmable logic controllers timers in Coq. IET Software, Institution of Engineering and Technology, 2011. 〈inria-00612410〉

Partager

Métriques

Consultations de la notice

155