Modeling And Verification Of Reconfigurable Discrete Event Control Systems

Most modern technological systems rely on complicated control technologies, computer technologies, and networked communication technologies. Their dynamic behavior is intri-cate thanks to the concurrence and conflict of various signals. Such complex systems can be studied as discrete event control systems (DECSs) by ignoring their detailed continuous variable processes. Dynamic reconfigurable systems are a trend of all future technological systems, not only limited to safety-critical high-end systems like nuclear control systems and flight control systems, but also other systems like vehicle electronic systems, manufac-turing systems, etc. In order to meet control requirements continuously, such a dynamic reconfigurable system is expected to be able to actively adjust its configuration at runtime by modifying its components, connections among components, and data, while changes are detected in the internal/external execution environment. These changes include faults of partial components, blocking on communication networks, unknown disturbances, and user requirements. Model based design methodologies attract wide attention since they can de-tect system defect earlier during the system design stage, increase system reliability, and decrease time cost on system development. An accurate, compact, and easily to be analyzed formal model is the first step of model based design methods. Based on this, formal verifi-cation is an expected effective method to completely check if a designed system meets all requirements and to improve a system design scheme. This dissertation deals with formal modeling and verification of reconfigurable discrete event control systems (RDECSs).The formalism Net Condition/Event System (NCES) is a modular extension of Petri nets. Its clear modularity fits the modeling requirements of RDECSs. This dissertation studies three possible reconfiguration scenarios of an NCES. They are the modification of places, transitions, and initial markings, respectively. Accordingly, an NCES based nested state machine is developed to cope with their implementation. The correctness of the final NCES model is checked by the software SESA, where the functional properties are specified by Computation Tree Logic (CTL) and its extension extended CTL (eCTL).It is found that the direct modeling of RDECSs by using NCESs may greatly burden the subsequent verification. To this end, a new formalism Reconfigurable Timed Net Condi-tion/Event System (R-TNCES) is proposed. An R-TNCES is composed of a control module and a behavior module. The behavior module is a set of superposed Timed Net Condi-tion/Event Systems (TNCESs). The control module is a set of reconfiguration functions. These reconfiguration functions control the switching among TNCESs in the behavior mod-ule. Furthermore, considering the similarity among TNCESs of the behavior module, a level-by-level verification method is developed to control the verification complexity of an R-TNCES.Consistency is one of the most important properties of distributed reconfigurable systems. This dissertation develops a novel coordination method for such systems. All reconfigurable subsystems are modeled by R-TNCESs. A virtual coordinator is built and a communication protocol among it and the subsystems is applied. Such a method has two benefits:1) an optimal global reconfiguration scenario is obtained and 2) the number of exchanged mes-sages is reduced. All reconfiguration processes are verified with the help of SESA, where functional and temporal properties are specified by CTL, eCTL, and Timed CTL (TCTL).Finally, in order to analyze the detailed system behavior during dynamic reconfiguration processes of RDECSs. This dissertation further extends the R-TNCES formalism. Reconfig-uration functions are newly assigned with action ranges and concurrent decision functions. In addition, the firing rules of events are updated such that the concurrence of reconfigura-tion events and normal events are conditionally allowed. Similarly, to check the correctness of the extension, SESA is applied. A reconfigurable and energy-efficient vehicle assembly line is applied to illustrate all the work of this part.