Contract Based Verification of IEC 61499
Ref: CISTER-TR-161106 Publication Date: 18 to 21, Jul, 2016
Contract Based Verification of IEC 61499
Ref: CISTER-TR-161106 Publication Date: 18 to 21, Jul, 2016Abstract:
The IEC 61499 standard proposes an event drivenexecution model for component based (in terms of FunctionBlocks), distributed industrial automation applications. However,the standard provides only an informal execution semantics, thusin consequence behavior and correctness relies on the designdecisions made by the tool vendor. In this paper we presentthe formalization of a subset of the IEC 61499 standard inorder to provide an underpinning for the static verification ofFunction Block models by means of deductive reasoning. Specifically,we contribute by addressing verification at the component,algorithm, and ECC levels. From Function Block descriptions, enrichedwith formal contracts, we show that correctness of componentcompositions, as well as functional and transitional behaviorcan be ensured. Feasibility of the approach is demonstrated bymanually encoding a set of representative use-cases in WhyML,for which the verification conditions are automatically derived(through the Why3 platform) and discharged (using automaticSMT-based solvers). Furthermore, we discuss opportunities andchallenges towards deriving certified executables for IEC 61499models.
Per Lindgren
Marcus Lindner
David Pereira
Luis Miguel Pinho14th International Conference on Industrial Informatics (INDIN 2016), Factory Automation.
Poitiers, France.
Record Date: 21, Nov, 2016