A Refinement-Based Validation Method for Programmable Logic Controllers

Hai Wan 1 Xiaoyu Song 1 Gang Chen 2 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 computer-based industrial applications. Timers play a pivotal role in PLC real-time embedded system applications. The paper addresses the formal validation of PLC systems with timers in the theorem proving system Coq. The timer behavior is characterized formally. A refinement validation methodology is presented in terms of an abstract model and a concrete model. The refinement is calibrated by a mapping relation. The soundness of the methodology is shown in the proving system. An illustrative case study demonstrates the eectiveness of the approach.
Type de document :
Communication dans un congrès
The 10th International Conference on Quality Software, Jul 2010, Zhangjiajie, Hunan, China. 2010
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-00516014
Contributeur : Hai Wan <>
Soumis le : mardi 8 mars 2011 - 07:00:23
Dernière modification le : mardi 17 avril 2018 - 11:30:09
Document(s) archivé(s) le : jeudi 9 juin 2011 - 02:17:26

Fichier

paper_20100104.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00516014, version 1

Collections

Citation

Hai Wan, Xiaoyu Song, Gang Chen, Ming Gu. A Refinement-Based Validation Method for Programmable Logic Controllers. The 10th International Conference on Quality Software, Jul 2010, Zhangjiajie, Hunan, China. 2010. 〈inria-00516014〉

Partager

Métriques

Consultations de la notice

180

Téléchargements de fichiers

121