Parameterized Specification and Verification of PLC Systems in Coq

Hai Wan 1 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) represent a typical class of embedded software systems. They are widely used in safety-critical industrial applications, such as railways, automotive applications, etc. The paper presents a novel method to specify and verify PLC software systems with the theorem proving system Coq. Dependent inductive data types are har- nessed to represent the component specifications. Modular and parameterized specification and verification are proposed. An illustrative example demonstrates the effectiveness of the method.
Type de document :
Communication dans un congrès
4th IEEE International Symposium on Theoretical Aspects of Software Engineering, Aug 2010, Taipei, Taiwan. 2010
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00516016
Contributeur : Hai Wan <>
Soumis le : mardi 8 mars 2011 - 07:00:30
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29
Document(s) archivé(s) le : jeudi 9 juin 2011 - 02:18:54

Fichier

Modular_and_Parameterized_veri...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00516016, version 1

Collections

Citation

Hai Wan, Xiaoyu Song, Ming Gu. Parameterized Specification and Verification of PLC Systems in Coq. 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, Aug 2010, Taipei, Taiwan. 2010. 〈inria-00516016〉

Partager

Métriques

Consultations de la notice

174

Téléchargements de fichiers

123