Zur Seitenansicht
 

Titelaufnahme

Titel
Component-based Deductive Verification of Cyber-Physical Systems / submitted by Andreas Müller
Weitere Titel
Komponenten-basierte deduktive Verifikation von Cyber-Physischen Systemen
AutorInnenMüller, Andreas
Beurteiler / BeurteilerinSchwinger, Wieland ; Platzer, Andre
Betreuer / BetreuerinSchwinger, Wieland
ErschienenLinz, 2017
Umfangxvi, 194 Seiten : Illustrationen
HochschulschriftUniversität Linz, Dissertation, 2017
Anmerkung
Abweichender Titel laut Übersetzung der Verfasserin/des Verfassers
SpracheEnglisch
Bibl. ReferenzOeBB
DokumenttypDissertation
Schlagwörter (DE)Komponenten-basierte Verifikation/Cyber-physische Systeme/Deduktive Verifikation
Schlagwörter (EN)component-based verification/cyber-physical systems/deductive verification
Schlagwörter (GND)Axiomatik / Verifikation / Cyber-physisches System
URNurn:nbn:at:at-ubl:1-19087 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist gemäß den "Hinweisen für BenützerInnen" verfügbar
Dateien
Component-based Deductive Verification of Cyber-Physical Systems [9.65 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Englisch)

Cyber-physical systems (CPS) are pervasively embedded into our lives and increasingly act in close proximity to as well as with direct impact on humans. Because of their safety-criticality, formal verification techniques that guarantee correctness properties for all of the infinitely many possible states of a CPS are of paramount importance. Since formal verification of CPS is known to be undecidable for realistic models, techniques to handle system complexity are needed. Verification methods based on hybrid automata focus on full automation and are therefore restricted to less expressive classes of CPS, while deductive verification methods rely on human guidance to make progress despite undecidability. To make human guidance possible, however, the inherent complexities of CPS practically mandate techniques to handle system complexity. This thesis introduces a component-based verification approach for CPS based on deductive verification. ^Crucially, the approach builds safety proofs about systems from smaller component proofs without analyzing the systems as a whole. As a result, the approach reduces verification complexity while simultaneously increasing proof reusability and maintainability. We develop the approach in three stages of increasing generality and suitable to various areas of application. First, we focus on modeling and verification of large traffic networks, and aim at avoiding traffic breakdowns on roads (i.e., the number of cars must not exceed the road's capacity) as fixed safety property. Second, we generalize flow exchange between components to instantaneous, lossless information exchange being restricted to globally known regions (e.g., robot position relative to a fixed reference point) and allow arbitrary safety properties. ^Third, we relate component time to global system time in order to describe information exchange history in terms of the magnitude of change and rate of change (e.g., robot position relative to previous position some time ago). We show the applicability of these three approaches by modeling examples from traffic control, vehicle control and autonomous robots. The results indicate that, compared to monolithic analysis, our approaches reduce verification effort, increase proof automation, facilitate reuse of component proofs and increase the overall maintainability of a verified CPS.

Zusammenfassung (Deutsch)

Cyber-physische Systeme (CPS) sind untrennbar mit unserem täglichen Leben verbunden und arbeiten immer mehr in unserer direkten Umgebung bzw. mit direktem Einfluss auf Menschen. Weil die Sicherheit solcher Systeme dadurch besonders kritisch ist, sind formale Verifikationstechniken, die die Sicherheit aller möglichen Zustände eines solchen CPS sicherstellen, von größter Wichtigkeit. Da formale Verifikation von realistischen cyber-physischen Modellen aber unentscheidbar ist, sind Techniken zur Komplexitätsreduktion (z.B. zerlegen eines Systems in kleinere Teilsysteme) unabdingbar. In dieser Dissertation präsentieren wir einen komponentenbasierten Ansatz zur Verifikation von CPS, basierend auf deduktiver Verifikation. Der Ansatz ermöglicht es, von kleineren Komponenten-Beweisen auf systemweite Sicherheitseigenschaften zu schließen, ohne das System als Ganzes analysieren zu müssen. ^Dadurch reduziert sich die Verifikationskomplexität, während gleichzeitig die Wiederverwendbarkeit und Wartbarkeit von Beweisen erhöht wird. Wir entwickeln den Ansatz in drei Schritten, welche die Analyse von immer allgemeineren Systemen erlauben. Zuerst fokussieren wir uns auf Modellierung und Verifikation von großen Verkehrsnetzen, mit dem festen Ziel einen Zusammenbruch des Fließverkehrs zu verhindern (d.h., es dürfen sich nie mehr Fahrzeuge gleichzeitig auf einer Straße befinden, als erlaubt). Im nächsten Schritt verallgemeinern wir Kommunikation und Sicherheitseigenschaften, weg von Verkehrskomponenten und Fließverkehr, hin zu beliebiger Informationsweitergabe und frei wählbaren Sicherheitseigenschaften. Die kommunizierten Werte sind dabei durch global festgelegte Regionen beschränkt (z.B. die Position eines Roboters, relativ zu einem festgelegten Referenzpunkt). ^Im letzten Schritt synchronisieren wir die Zeit zwischen Komponenten und dem Gesamtsystem und ermöglichen Zugriff auf früher kommunizierte Werte, um Aussagen über die Größenordnung und die Rate der Werteänderung treffen zu können (z.B., die Position eines Roboters, relativ zu seiner letzten Position und der Zeit die seitdem vergangen ist). Wir zeigen die Anwendbarkeit unserer Ansätze anhand von Fallstudien aus den Bereichen Straßenverkehr, Fahrzeugsteuerung und autonome Roboter. Die Ergebnisse legen nahe, dass unsere Ansätze tatsächlich zu einer Verringerung der Beweiskomplexität führen und gleichzeitig die Wiederverwendbarkeit und Wartbarkeit von Beweisen erhöhen.

Statistik
Das PDF-Dokument wurde 30 mal heruntergeladen.