Abstract
This study deals with the formal modeling and verification of reconfigurable discrete event control systems (RDECSs). The behavior of an RDECS is represented by that of control components (CCs) and the communication among them. A new formalism, called Reconfigurable Timed Net Condition/Event Systems (TNCES) (R-TNCES), is proposed for the optimal functional and temporal specification of RDECS, which is defined by a behavior module and a control module. The former is a union of various superposed TNCESs, where TNCES-based CC modules are basic units. The latter is a set of reconfiguration functions dealing with the automatic transformations of these TNCESs in response to errors or user requirements by enabling or disabling CC modules, changing condition signals and/or event signals among them, and also treating the state feasibility before and after reconfigurations. To control the verification complexity of R-TNCES, a layer-by-layer verification method is developed, where the similarities of different TNCESs in the behavior module are considered. The contribution of this original paper is applied to a benchmark production system.