Service-oriented design and verification of hybrid systems

Nowadays, 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.

Author dc:creator

• Liebrenz, Timm

Advisors dc:contributor.advisor

• Glesner, Sabine
• Herber, Paula

Licence dc:rights.uri

• https://creativecommons.org/licenses/by/4.0/

Language dc:language.iso

en

Identifier URI

https://doi.org/10.14279/depositonce-17168

OAI identifier oai:identifier

oai:depositonce.tu-berlin.de:11303/18721