NCES-based modelling and CTL-based verification of reconfigurable embedded control systems

This paper (This work is done in the research laboratory of Prof. Dr. Hans-Michael Hanisch at the Martin Luther University in Germany, and it is supported by the Alexander von Humboldt foundation in Germany under the reference TUN1127196STP.) deals with automatic reconfigurations of safe embedded control systems following the component-based International Industrial Standard IEC61499 in which a Function Block (FB) is an event triggered software component owning data and a control application is a network of blocks. We define a new semantics of reconfigurations that allow automatic improvements of system performances at run-time even if there are no hardware faults. We apply this new semantics on two Benchmark Production Systems developed in our research laboratory according to this industrial technology. We classify thereafter into three forms all possible reconfiguration scenarios to be applied at run-time by a well-defined agent in order to adapt the system to its environment according to well-defined conditions. The agent is modelled by nested state machines according to the formalism Net Condition/Event Systems (NCES) which is an extension of Petri nets. In order to satisfy user requirements, we specify functional and non-functional properties according to the well-known temporal logic “Computation Tree Logic” (CTL) as well as its extensions eCTL and TCTL, and we apply the model checker SESA to check the whole agent-based architecture of the reconfigurable system.