Model checking optimization of safe Control Embedded Components with refinement

This paper deals with model checking optimization of Software Embedded Control Components by applying refinement. We introduce a Software Embedded Control Component 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. To ensure safety, an intelligent software agent controls the plant and applies automatic reconfiguration whenever a physical error occurs in the plant. We propose in this paper to model checking these different reconfigurations through a refinement method realized step by step. The contributions of the paper are applied to two Benchmark Production Systems available in our research laboratory.