Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Hehua Zhang <>
Submitted on : Friday, July 29, 2011 - 6:58:50 AM
Last modification on : Monday, December 14, 2020 - 3:30:22 PM


  • HAL Id : inria-00612416, version 1



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. ⟨inria-00612416⟩



Record views