Edola: A Domain Modeling and Verification Language for PLC Systems

Hehua Zhang 1 Ming Gu 1 Xiaoyu Song 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 : Formal modeling and verification of PLC systems become paramount in engineering applications. This paper presents a novel PLC domain-specific modeling language Edola. Important characteristics of PLC embedded systems, such as reactivity, scan cycling, real-time and property patterns, are embodied in the language design. Formal verification methods, such as model checking and automatic theorem proving, are supported in Edola modeling. The TLA+ specification language constitutes an intermediate language layer between Edola and the verification tools, enhancing a large degree of reusability. A prototype IDE for Edola and its seamless integration of a model checker TLC and an automatic theorem prover Spass for verification are implemented. A case study illustrates and validates the applicability of the language.
Type de document :
Communication dans un congrès
The Sixth International Conference on Software Engineering (ICSEA 2011), Oct 2011, Barcelona, Spain. 2011
Liste complète des métadonnées

https://hal.inria.fr/inria-00612416
Contributeur : Hehua Zhang <>
Soumis le : vendredi 29 juillet 2011 - 06:58:50
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29

Identifiants

  • HAL Id : inria-00612416, version 1

Collections

Citation

Hehua Zhang, Ming Gu, Xiaoyu Song. Edola: A Domain Modeling and Verification Language for PLC Systems. The Sixth International Conference on Software Engineering (ICSEA 2011), Oct 2011, Barcelona, Spain. 2011. 〈inria-00612416〉

Partager

Métriques

Consultations de la notice

155