Modeling and verification of reconfigurable discrete event control systems
Jiafeng Zhang · Publications of the UdS (Saarland University) · 2015
Most modern technological systems rely on complicated control technologies, computer technologies, and networked communication technologies. Their dynamic behavior is intricate due to the concurrence and conflict of various signals. Such complex systems are studied as discrete event control systems (DECSs), while the detailed continuous variable processes are abstracted. Dynamic reconfigurable systems are the trend of all future technological systems, such as flight control systems, vehicle electronic systems, and manufacturing systems. In order to meet control requirements continuously, such a dynamic reconfigurable system is able to actively adjust its configuration at runtime by modifying ist components, connections among components and data, while changes are detected in the internal/external execution environment. Model based design methodologies attract wide attention since they can detect system defect earlier, increase system reliability, and decrease time and cost on system development. An accurate, compact, and easy formal model to be analyzed is the first step of model based design methods. Formal verification is an expected effective method to completely check if a designed system meets all requirements and to improve the system design scheme. Considering the potential benefits of Timed Net Condition/Event Systems (TNCESs) in modeling and analyzing reconfigurable systems, this dissertation deals with formal modeling and verification of reconfigurable discrete event control systems (RDECSs) based on them. Die meisten modernen technologischen Systeme benotigen aufwandige Steuerungs-, Rechner- und Kommunikationstechnologien. Aufgrund von Nebenlaufigkeit und Konflikten ergibt sich ein kompliziertes dynamisches Verhalten. Derartige komplexe Systeme werden dadurch untersucht, dass man sie als ereignisdiskrete Steuerungssysteme (Discrete Event Control Systems, DECSs) betrachtet und dabei die detaillierten unterlagerten kontinuierlichen Prozesse abstrahiert. Um die Anforderungen an die Steuerung durchgangig erfullen zu konnen adaptieren sich dynamische rekonfigurierbare Systeme zur Laufzeit durch Modifikation ihrer Komponenten, deren Verbindungen untereinander und der gespeicherten Daten, sobald Anderungen in der internen oder externen Umgebung festgestellt werden. Beispiele fur dynamische Rekonfigurierbare Systeme finden sich in der Luftfahrt, im Automobilbereich aber auch in Fertigungssystemen. Modellbasierte Entwicklungsmethoden erfreuen sich zunehmender Beliebtheit, da sie es erlauben Fehler fruher im Entwicklungsprozess aufzudecken und damit zu hoherer Systemverfugbarkeit bei verkurzter Entwicklungszeit fuhren. Ein formales Modell des Systems bildet hierbei den ersten wichtigen Schritt. Durch formale Verifikation kann dieses Modell effektiv und vollstandig uberpruft und ggf. verbessert werden. Eine geeignete Modellform hierfur sind Timed Net Condition/Event Systems (TNCESs). Die vorliegende Dissertation befasst sich mit der Anwendung von TNCES zur Modellierung und Verifikation rekonfigurierbarer ereignisdiskreter Steuerungssysteme (RDECSs).