Edola: A Domain Modeling and Verification Language for PLC Systems

Formal modeling and verification of PLC systems become paramount in engineering applications. The 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.