Model-checking for the functional safety of Control Component-based heterogeneous embedded systems

This paper¹ deals with the model checking of Safe Heterogeneous Embedded Control Systems following different component-based technologies or implemented according to different Architecture Description Languages (ADL) used today in industry. The purpose is to reduce their time to market by exploiting various execution environments and different rich libraries. A ¿Control Component¿ is defined in our research work as an event-triggered software unit composed of an interface for any external interactions and an implementation allowing control actions of physical processes. A control system is assumed to be a composition of components with precedence constraints to control the plant according to well-defined execution orders. We define an agent-based architecture where the agent controls the environment evolution and applies automatic reconfigurations when hardware errors occur at run-time to guarantee a functional safety of the whole system. We model the architecture according to the formalism Net Condition/Event Systems (abbr. NCES), and apply the model checker SESA to check functional properties described according to the well-known Computation Tree Logic (abbr. CTL). Our purpose is to check that whenever an error occurs at run-time, the agent behaves as described in user requirements by activating Control Components and deactivating others to guarantee a functional safety of the whole system. A Benchmark Production System is used in this research work to explain our contribution.