Verification of hierarchical IEC 61499 component systems with behavioral event contracts

Behavioral event contracts constrain the ordering of input events received and possible output events returned from a software component. Interface automata as introduced by de Alfaro and Henzinger are a light-weight formalism that allow capturing such temporal aspects of software component interfaces and the associated theory allows answering such fundamental questions as interface compatibility, component composition, and refinement. The work presented in this paper applies the results from the theory of interface automata in a hierarchical design and verification approach for IEC 61499 automation solutions. IEC 61499 adapters and service sequences are used for specification of rich behavioral component interfaces. In this approach, components are built hierarchically in master-slave arrangements where each component defines a provided interface contract for its upper-level and specifies required interface contracts for its subcomponents. Verification methods allows verifying if a component uses all its subcomponents according to their contracts, allows checking if a concrete component satisfies a given contract, and allows computing an abstraction of a component representing its externally visible behavior.