TY - GEN
T1 - Verification of Hierarchical IEC 61499 Component Systems with Behavioral Event Contracts
AU - Prähofer, Herbert
AU - Zoitl, Alois
PY - 2013
Y1 - 2013
N2 - 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 specifica-
tion 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 com-
ponent 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.
AB - 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 specifica-
tion 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 com-
ponent 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.
UR - http://www.ssw.jku.at/Research/Papers/
M3 - Conference proceedings
SN - 9781479907519
VL - CFP13INI-USB
T3 - IEEE Catalog
SP - 578
EP - 585
BT - USB Proceedings 2013 11th IEEE International Conference on Industrial Informatics (INDIN)
PB - IEEE
ER -