Service-oriented design and verification of hybrid systems

dc.contributor.advisorGlesner, Sabine
dc.contributor.advisorHerber, Paula
dc.contributor.authorLiebrenz, Timm
dc.contributor.grantorTechnische Universität Berlin
dc.contributor.refereeGlesner, Sabine
dc.contributor.refereeGiese, Holger
dc.contributor.refereeHerber, Paula
dc.contributor.refereeSchlingloff, Holger
dc.date.accepted2022-07-05
dc.date.accessioned2023-03-31T15:20:18Z
dc.date.available2023-03-31T15:20:18Z
dc.date.issued2023
dc.description.abstractNowadays, cyber-physical systems find application in many areas. These systems consist of multiple control components that interact with each other and with the physical environment. Model-driven development methods are used to handle their complexity and to ease their development. Furthermore, variability in the model design enables to customize a system for different environments. In safety-critical areas, where faulty behavior can injure or even kill people, it is desirable that the development and quality assurance of these systems is performed rigorously. Cyber-physical systems have properties that make their development and quality assurance challenging. They contain hybrid behavior, which is the interaction of discrete changes and continuous behavior that is described by differential equations. Data flow-oriented modeling languages that are used in industry aim at enabling the comprehensible and fast development of hybrid control systems. However, they lack formal semantics, which precludes the application of rigorous verification methods and thus makes it impossible to provide guarantees about the behavior of the modeled systems. Formal modeling languages enable us to precisely model the mathematical processes and to formally verify that the system fulfills its requirements. However, correct behavior for each system variant must be ensured, which requires high effort, and formal approach often have scalability issues when handling industrially used models. Two major barriers prevent formal methods from being applied in practice: The lack of formal semantics of industrially used modeling languages, but also the high cost of rigorous formal verification. In this thesis, we present an approach for the service-oriented design and verification of hybrid control systems. We define the concept of a Service for hybrid systems, with which we can formally define the functionality of the system and customize it for different contexts. As representative for data flow-oriented modeling languages, we present a formalization for Simulink into differential dynamic logic (dL), which is a formal language to design and verify hybrid systems. Our formalization enables the formal verification of hybrid Simulink models. With the verification results, we create hybrid contracts that describe the interface behavior of these services containing hybrid behavior. Additionally, we present an abstraction mechanism for services with hybrid contracts that enables the scalable verification of systems consisting of interacting services. With the addition of a feature model, we enable the customization for services for the reuse in different contexts. We have created a framework that implements our service-oriented design in Simulink and provides an automatic transformation of Simulink models into dL to enable the service-oriented design and verification of Simulink models. The hierarchical nature of services enables the development of larger models that are verifiable. Our approach combines the strengths of model-driven development of hybrid systems with the power of formally ensuring the correct behavior of modeled systems under all circumstances. We provide a formal foundation for hybrid Simulink models, for which we have developed an automatic transformation of Simulink models into dL. With our abstraction with hybrid contracts, we can provide safety guarantees for larger systems that consist of multiple interacting services. With a feature model and automatic service generation, we enable easy customization of services and their reuse. We demonstrate the applicability of our approach with different experimental results.en
dc.description.abstractIn der heutigen Zeit finden cyber-physische Systeme in vielen Bereichen Anwendung. Diese bestehen aus Steuerelementen, die miteinander und mit der Umgebung interagieren. In der Praxis werden modellgetriebene Entwicklungsmethoden verwendet, um die Entwicklung zu vereinfachen. Durch das Bereitstellen von Variabilität im Design des Modells kann das System zur Verwendung in verschiedenen Umgebungen vorbereitet werden. In sicherheitskritischen Bereichen, bei welchen fehlerhaftes Verhalten zu Verletzungen oder Tod führen kann, ist ausgiebige Qualitätssicherung während der Entwicklung wichtig. Die Eigenschaften von cyber-physischen Systemen erschweren deren Entwicklung und Qualitätssicherung. Sie weisen hybrides Verhalten auf, welches diskretes und kontinuierliches Verhalten kombiniert. Datenfluss-orientierte Sprachen, welche in der Industrie verwendet werden, ermöglichen das schnelle Erstellen von hybriden Steuersystemen mithilfe von nachvollziehbaren Modellen. Jedoch haben diese Sprachen keine formale Semantik und ermöglichen es nicht Garantien über das korrekte Systemverhalten zu liefern. Formale Modellierungssprachen ermöglichen es präzise die mathematischen Prozesse im Modell dazustellen und ermöglichen es formal zu prüfen, ob das modellierte System die Anforderungen erfüllt. Beim Bereitstellen von Variabilität muss zusätzlich für jede Variante korrektes Verhalten sichergestellt werden. Zusätzlich skalieren formale Ansätze schwer für Modellgrößen, die in der Praxis relevant sind. Die folgenden Barrieren behindern die Anwendung von Formalen Methoden in der Praxis: Die fehlende formale Semantik für in der Industrie verwendete Modellierungssprachen und hohe Kosten der formalen Verifikation. In dieser Dissertation stellen wir einen Ansatz zur Service-Orientierten Entwicklung und Verifikation für hybride Steuerungssystem vor. Wir definieren den Begriff eines Service für Hybride Systeme, der es ermöglicht formal die Funktionalität von Komponenten zu erfassen und an verschiedene Kontexte anzupassen. Wir nehmen beispielhaft die datenflussorientierte Modellierungssprache Simulink und präsentieren eine Formalisierung in der formalen Semantik von Differential Dynamic Logic (dL). Wir erstellen hybrid contracts, welche formal das Interfaceverhalten der Services erfassen. Zudem präsentieren wir einen Service-Abstraktionsmechanismus, der es ermöglicht Eigenschaften von größeren Systemen mit integrierten Services zu verifizieren. Außerdem beinhaltet unsere Definition von Services ein Feature Modell, das es ermöglicht Teile des Services zu modifizieren, um diesen für andere Anwendungsfälle anzupassen. Wir haben unsere Konzepte in einem Ansatz für Simulink implementiert und ermöglichen damit die Service-Orientierte Entwicklung und Verifikation für Simulink. Die hierarchische Natur von unseren Services ermöglicht die Entwicklung und Verifikation von größeren Systemen, die aus interagierenden Services bestehen und die wiederum formal verifiziert werden können. Unser Ansatz kombiniert Stärken modellgetriebener Entwicklung von hybriden Systemen mit den formalen Garantien, die korrektes Systemverhalten unter allen Umständen sicherstellen. Wir stellen eine formale Basis für hybride Simulink Modelle bereit, für welche wir eine automatische Transformation von Simulink nach dL entwickelt haben. Wir ermöglichen Sicherheitsgarantien mithilfe unserer Abstraktion über hybrid contracts für größere Systeme, die aus interagierenden Services bestehen. Über ein Feature Modell und einer automatischen Erstellung von Services, ermöglichen wir die Anpassung von Services für andere Umgebungen und erhöhen ihre Wiederverwendbarkeit. Wir demonstrieren die Anwendbarkeit unseres Ansatzes mithilfe von verschiedenen experimentellen Ergebnissen.de
dc.identifier.urihttps://depositonce.tu-berlin.de/handle/11303/18721
dc.identifier.urihttps://doi.org/10.14279/depositonce-17168
dc.language.isoen
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.subject.ddc000 Informatik, Informationswissenschaft, allgemeine Werke::000 Informatik, Wissen, Systeme::000 Informatik, Informationswissenschaft, allgemeine Werke
dc.subject.otherformal verificationen
dc.subject.otherhybrid systemsen
dc.subject.otherservice-orienteden
dc.subject.otherSimulinken
dc.subject.otherKeYmaera Xen
dc.subject.otherformale Verifikationde
dc.subject.otherhybride Systemede
dc.subject.otherservice-orientiertde
dc.titleService-oriented design and verification of hybrid systemsen
dc.title.translatedService-orientiertes Design und Verfikation von hybriden Systemende
dc.typeDoctoral Thesis
dc.type.versionacceptedVersion
dcterms.rightsHolder.referenceDeposit-Lizenz (Erstveröffentlichung)
tub.accessrights.dnbfree
tub.affiliationFak. 4 Elektrotechnik und Informatik::Inst. Softwaretechnik und Theoretische Informatik::FG Software and Embedded Systems Engineering
tub.publisher.universityorinstitutionTechnische Universität Berlin

Files

Original bundle
Now showing 1 - 1 of 1
Loading…
Thumbnail Image
Name:
liebrenz_timm.pdf
Size:
3.49 MB
Format:
Adobe Portable Document Format
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
4.23 KB
Format:
Item-specific license agreed upon to submission
Description:

Collections