A Maneuver-Centric Formal Engineering Approach for Cyber-Physical Systems
In present days, cyber-physical systems (CPSs) play an increasingly vital role in in our everyday lives and effectively demonstrate how we, as a society, aim at leveraging technology to mitigate human error. Automated vehicles, robots, and aircraft are only a few prime examples of such systems that combine digital computations, such as control algorithms, with physical motion in space. As such systems become more complex, designing them becomes more challenging. The main reason is their inherently safety-critical and hybrid nature, which not only requires highly standardized quality assurance of the running software, but also sophisticated preplanning. However, these two challenges come with a cost, such as scalability issues during the software development process or the need for high expertise. Consequently, we hypothesize that the key to designing safe behaviors for CPSs in a manageable fashion and maximizing trust early on mandates a software engineering process that (1) prioritizes appropriate abstractions in the early design phase (i.e., starting with requirements engineering), but (2) builds formal safety proofs from smaller parts at each stage of the process to establish correctness of the whole system. In this thesis, we make several contributions to establish such a formal engineering process, where safety proofs at each development step are built by applying deductive verification. In particular, we focus on three key areas namely (1) planning, modeling, and analyzing safe behavior of cyber-physical systems, (2) deriving correct implementations with the goal of validating them through simulation, and (3) improving deductive verification applied on source-code level. As a starting point for modeling safe CPS behavior, we introduce a formal framework based on skill graphs, a graph-based modeling formalism for decomposing the overall behavior of CPSs into isolated and verifiable maneuvers (e.g., following a leading vehicle in the context of automated driving). For specifying and verifying skill graphs, we combine them with a contract theory and model parts of their behavior by means of hybrid programs. Crucially, skill graphs can be composed to exhibit more complex maneuvers built from simpler ones. This compositional nature of our framework enables the reduction of verification complexity while it simultaneously prioritizes proof reuse. Furthermore, we introduce a methodology for refining verified skill graphs to component-based architectures. In particular, nodes in a skill graph are mapped to components and edges correspond to component connectors. While certain components can be generated automatically, safe component behavior of to-be-developed components is ensured by applying the correctness-by-construction paradigm. Subsequent simulations of the executable and verified maneuvers allow to validate their requirements in a diverse set of scenarios. Finally, we discuss two techniques in the context of formal specification and deductive program verification with the goal of bridging the gap between software engineering practices and formal methods. First, we assess to what extent a mutation analysis is valid and practical for measuring the precision of software contracts, which is an invaluable metric for software developers working with formal specifications. Second, we present a technique to increase the performance and success rate of the automatic proof search of configurable program verifiers by examining the influence of control parameters.
Cyber-physische Systeme nehmen eine zunehmend wichtige Rolle in unserem Alltag und unserer Gesellschaft ein, und haben das Ziel, durch technologischen Fortschritt und Automatisierung menschliches Fehlverhalten zu minimieren. Zu den Einsatzbereichen gehören autonome Straßenfahrzeuge, autonome Roboter, oder aber auch Luftfahrzeuge. Cyber-physische Systeme vereinen dabei digitale Software mit mechanischen und elektrischen Komponenten im physischen Raum, was zu schwerwiegendem Fehlverhalten in der realen Welt führen kann. Durch die steigende Komplexität erhöht sich ebenfalls auch das benötigte Expertenwissen während der Entwicklungsphase solcher Systeme. Um dennoch die Sicherheit zu gewährleisten, muss besonderes Augenmerk auf die Qualitätssicherung im Entwicklungsprozess gelegt werden. Vorzugsweise werden hier Konzepte der formalen Verifikation angewendet, die eine Zertifizierung der Korrektheit der ausgelieferten Software garantieren. Der inhärente Nachteil ist allerdings die schlechte Skalierung und das benötige Expertenwissen solcher Methoden. Wir nehmen daher an, dass ein erfolgreicher Entwicklungsprozess mindestens zwei Konzepte miteinander vereint: hohe Abstraktion in der frühen Entwicklungsphase und formale, modulare Beweisführung kleinerer Komponenten mit dem Ziel die Korrektheit des Gesamtsystems zu attestieren. Diese Arbeit leistet wichtige Beiträge, um sich einen solchen formalen Entwicklungsprozess anzunähern. Insbesondere werden dabei drei Kernbereiche beleuchtet: (1) Planung, Modellierung, und beweisgestützte Verifikation von Cyber-physischen Systemen während der Designphase, (2) Ableitung korrekter Implementierungen, die virtuell simuliert werden können, und (3) Verbesserung der Anwendung der deduktiven Verifikation für End-Nutzer auf Implementierungsebene. Um sicheres Verhalten modellieren und verifizieren zu können, entwickeln wir in dieser Arbeit zunächst ein formales Konzept basierend auf Fähigkeitsgraphen (engl.: skill graphs). Fähigkeitsgraphen stellen eine grafische Notation zur Beschreibung von isolierten Fahrmanövern dar (z.B. Abstandsautomat), die dabei besonderen Fokus auf Modularität legt. Zur Spezifikation und Verifikation kombinieren wir Fähigkeitsgraphen mit Verträgen und hybriden Programmen. Die Modularität von Fähigkeitsgraphen erlaubt es unter bestimmten Bedingungen, komplexere Manöver aus simpleren abzuleiten und Verifikationsresultate zu transferieren. Dies reduziert nicht nur die Beweiskomplexität, sondern verbessert auch die Wiederverwendung von bereits geleistetem Beweisaufwand. Neben der Verifikation solcher Modelle ist es auch wichtig, die grundlegenden Sicherheitsanforderungen auf Vollständigkeit hin zu validieren, was durch Simulation (d.h., virtuelle Ausführung unter Realbedingungen) der Manöver erreicht werden soll. Dafür stellen wir eine Methodik vor, um aus Fähigkeitengraphen komponentenbasierte Architekturen abzuleiten. Während ein Großteil dieser Ableitung automatisiert werden kann, so gibt es durch die hohe Abstraktion der Fähigkeitengraphen auch manuell fertig zu entwickelnde Komponenten. Um dennoch Korrektheit garantieren zu können, kombinieren wir diese Methodik mit dem Correctness-by-Construction Paradigma. Schlussendlich diskutieren wir zwei Probleme im Kontext der vertragsbasierten Spezifikation und deduktiven Verifikation mit dem Ziel, die vorherrschende Lücke zwischen Praktiken der Softwarenentwicklung und den Formalen Methoden zu verkleinern. Als erstes untersuchen wir, inwiefern eine Mutationsanalyse Erkenntnisse über die Vollständigkeit vertragsbasierter Spezifikationen ermöglicht. Anschließend präsentieren wir eine Technik, welche zum Ziel hat, die Effektivität und Effizienz des automatischen Beweisalgorithmus' konfigurierbarer Programmbeweiser zu steigern, indem wir den Einfluss von Kontrollparametern untersuchen.
Preview
Cite
Access Statistic
Rights
Use and reproduction:
