JZ_Diss_2015

Zhang, Jiafeng:
Modeling and Verification of Reconfigurable Discrete Event Control Systems.


Dissertation, Universität des Saarlandes, Saarbrücken, Germany, and

Xidian University, Xi'an, Shaanxi, P.R. China, July 31st, 2015.

Saarländische Universitäts- und Landesbibliothek, Saarbrücken, 2015

Abstract:

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 its 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.

Kurzfassung:

Die meisten modernen technologischen Systeme benötigen aufwändige Steuerungs-, Rechner- und Kommunikationstechnologien. Aufgrund von Nebenläufigkeit 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 durchgängig erfüllen zu können adaptieren sich dynamische rekonfigurierbare Systeme zur Laufzeit durch Modifikation ihrer Komponenten, deren Verbindungen untereinander und der gespeicherten Daten, sobald Änderungen in der internen oder externen Umgebung festgestellt werden. Beispiele für 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 früher im Entwicklungs­prozess aufzudecken und damit zu höherer Systemverfügbarkeit bei verkürzter Entwicklungszeit führen. Ein formales Modell des Systems bildet hierbei den ersten wichtigen Schritt. Durch formale Verifikation kann dieses Modell effektiv und vollständig überprüft und ggf. verbessert werden. Eine geeignete Modellform hierfür 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).

摘要

现代技术系统大多依赖于复杂控制技术、计算机技术和网络通信技术。由于信号并发、冲突等的存在，导致系统的动态行为错综复杂。因此，往往将这些系统抽象为离散事件控制系统来研究。动态可重构系统是未来复杂技术系统的趋势，如安全关键的核电系统、飞控系统和普通的汽车电子系统、自动化制造系统等。这种系统可以根据系统内、外执行环境的变化，如部分组件故障、网络阻塞、未知干扰、用户请求等，主动地修改当前构型的部分组件、组件间连接关系和数据等，使当前构型在线地转变为另一种构型，从而保证系统能够持续地满足控制需求。基于模型的设计方法能够较早发现复杂技术系统的设计缺陷、提高系统的可靠性、缩短开发系统所耗费的时间，因此被广泛地关注和应用。一个准确、简洁且易于分析的系统形式化模型是基于模型设计方法的第一步。形式化验证是一种能够全面测试被设计的系统是否满足需求和改进系统设计方案的一种有力措施。考虑到Timed Net Condition/Event Systems (TNCESs)在分析可重构系统方面的诸多潜在优势，本文研究的主要内容就是基于TNCESs的可重构离散事件控制系统的形式化建模与验证。