A Formal Perspective on IEC 61499 Execution Control Chart Semantics
Ref: CISTER-TR-150802 Publication Date: 20 to 22, Aug, 2015
A Formal Perspective on IEC 61499 Execution Control Chart Semantics
Ref: CISTER-TR-150802 Publication Date: 20 to 22, Aug, 2015Abstract:
The IEC 61499 standard proposes an event driven execution model for distributed control applications for which an informal execution semantics is provided. Consequently, run-time implementations are not rigorously described and therefore their behavior relies on the interpretation made by the tool provider. In this paper, as a step towards a formal semantics, we focus on the Execution Control Chart semantics, which is fundamental to the dynamic behavior of Basic Function Block elements. In particular we develop a well-formedness criterion that ensures a finite number of Execution Control Chart transitions for each triggering event. We also describe the first step towards the mechanization of the well-formedness checking algorithm in the Coq proof-assistant so that, ultimately, we are able to show, once andforall,thatthisalgorithmiseffectivelycorrectwithrespectto our proposed execution semantics. The algorithm is extractable from the mechanization in a correct-by-construction way, and can be directly incorporated in certified toolchain for analysis, compilation and execution of IEC 61499 models. As a proof of concept a prototype tool RTFM-4FUN has been developed. It performs well-formedness checks on Basic Function Blocks using the extracted algorithm’s code.
Per Lindgren
Marcus Lindner
David Pereira
Luis Miguel PinhoIEEE International Symposium on Parallel and Distributed Processing with Applications (ISPA 2015).
Helsinki, Finland.
Record Date: 22, Aug, 2015