Zur Seitenansicht
 

Titelaufnahme

Titel
Specification and verification for real-time coordination protocols of cyber-physical systems / by Stefan Dziwok ; supervised by Prof. Dr. Wilhelm Schäfer and Prof. Dr. Matthias Tichy
AutorDziwok, Stefan
BeteiligteSchäfer, Wilhelm In der Gemeinsamen Normdatei der DNB nachschlagen ; Tichy, Matthias In der Gemeinsamen Normdatei der DNB nachschlagen
ErschienenPaderborn, 2017
Ausgabe
Elektronische Ressource
Umfang1 Online-Ressource (XVI, 429 Seiten) : Diagramme
HochschulschriftUniversität Paderborn, Dissertation, 2017
Anmerkung
Tag der Verteidigung: 05.09.2017
Verteidigung2017-09-05
SpracheEnglisch
DokumenttypDissertation
URNurn:nbn:de:hbz:466:2-29447 Persistent Identifier (URN)
DOI10.17619/UNIPB/1-196 
Dateien
Specification and verification for real-time coordination protocols of cyber-physical systems [12.93 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

Cyber-physische Systeme (CPSs) sind die nächste Generation von eingebetteten Systemen, die fortwährend ihre Zusammenarbeit koordinieren, um anspruchsvolle Funktionen zu erfüllen. Die Koordination zwischen ihnen kann in Software mittels asynchroner Nachrichtenkommunikation realisiert werden. Um die funktionale Korrektheit der Software zu gewährleisten, ist aufgrund der Kritikalität dieser Systeme eine formale Verifikation wie z.B. Model Checking notwendig. Die Eingabesprache eines Model Checkers unterstützt jedoch domänenspezifische Aspekte wie asynchrone Kommunikation nicht direkt, wodurch diese vom Softwareingenieur mittels zahlreicher Modellelemente spezifiziert werden müssen. Dies ist hochgradig komplex und somit fehleranfällig. Im Rahmen dieser Arbeit wird eine modellgetriebene Methode zur domänenspezifischen Spezifikation und vollautomatischen Verifikation der nachrichtenbasierten Koordination von CPSs präsentiert. Mit Hilfe dieser Methode kann der Softwareingenieur die Koordination kompakt modellieren und muss nicht länger verstehen, wie seine Spezifikation auf der Ebene des Model Checkers ausgedrückt wird. Insgesamt wird die Komplexität für den Softwareingenieur somit deutlich handhabbarer. Bezüglich der Spezifikation einer solchen Koordination definiert die Arbeit eine domänenspezifische Sprache namens Real-Time Coordination Protocols (RTCPs). Darüber hinaus wird eine domänenspezifische Sprache zur Spezifikation von Verifikationseigenschaften eingeführt und Entwurfsmuster für RTCPs präsentiert, um die Anzahl der Modellierungsfehler zu senken.

Zusammenfassung (Englisch)

Cyber-physical systems (CPSs) are the next generation of embedded systems that heavily interact with each other and their environment to fulfill advanced functionality. The coordination between them may be realized in software by means of asynchronous message communication. Due to the criticality of these systems, a formal verification like model checking is required in order to guarantee the functional correctness of the software. However, the input language of a model checker does not directly support domain-specific aspects such as asynchronous communication. Thus, a software engineer has to specify them using numerous model elements. This is highly complex and, thus, error-prone. This thesis presents a model-driven method for the domain-specific specification and fully automatic verification of the message-based coordination of CPSs. By using this method, the software engineer can model the coordination in a compact manner and does no longer need to understand how his specification is represented at the level of the model checker. Consequently, this thesis makes the complexity for the software engineer more manageable. Concerning the specification of such a coordination, this thesis defines a domain-specific language called Real-Time Coordination Protocols (RTCPs). In addition, it introduces a domain-specific language for the specification of verification properties and design patterns for RTCPs to reduce the number of modeling errors.