Home // ICSEA 2011, The Sixth International Conference on Software Engineering Advances // View article

Edola: A Domain Modeling and Verification Language for PLC Systems

Authors:
Hehua Zhang
Ming Gu
Xiaoyu Song

Keywords: domain-specific modeling language; formal verification;PLC; TLA+

Abstract:
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. A prototype IDE for Edola and its seamless integration of a model checker TLC and an automatic theorem prover Spass are implemented. A case study illustrates and validates the applicability of the language.

Pages: 281 to 286

Copyright: Copyright (c) IARIA, 2011

Publication date: October 23, 2011

Published in: conference

ISSN: 2308-4235

ISBN: 978-1-61208-165-6

Location: Barcelona, Spain

Dates: from October 23, 2011 to October 29, 2011