摘要 : The article deals with Reconfigurable Embedded Control Systems following different Component-based Technologies and/or Architecture Description Languages used today in Industry. We define a Control Component as a software unit to ... 展开 The article deals with Reconfigurable Embedded Control Systems following different Component-based Technologies and/or Architecture Description Languages used today in Industry. We define a Control Component as a software unit to support control tasks of the system which is assumed to be a network of components with precedence constraints. We define an agent-based architecture to handle automatic reconfigurations under well-defined conditions by creating, deleting or updating components to bring the whole system into safe and optimal behaviors. To cover all possible reconfiguration forms, we model the agent by nested state machines according to the formalism Net Condition/Event Systems (abbr. NCES) which is an extension of Petri nets. We apply in addition a model checking to verify functional and extra-functional properties according to the temporal logic "Computation Tree Logic" (abbr. CTL). The goal is to check the agent's reactivity after any evolution of the environment. Several complex networks can implement the system such that each one is executed at a given time when a corresponding reconfiguration scenario is automatically applied by the agent. To check the correctness of each one of them, we apply in several steps a refinement-based approach that automatically specifies feasible Control Components according to NCES. The model checker SESA is automatically applied in each step to verify deadlock properties of new generated components, and is manually used to verify CTL-based properties according to user requirements. Two Industrial Benchmark Production Systems FESTO and EnAS available in our research laboratory are applied to explain the article's contributions. 收起