Gast ::
| 001 | 767529 | ||
| 005 | 20241028133739.0 | ||
| 024 | 7 | _ | |a HT020212073 |2 HBZ |
| 024 | 7 | _ | |a 38567 |2 Laufende Nummer |
| 024 | 7 | _ | |a 10.18154/RWTH-2019-08875 |2 datacite_doi |
| 037 | _ | _ | |a RWTH-2019-08875 |
| 041 | _ | _ | |a English |
| 082 | _ | _ | |a 004 |
| 100 | 1 | _ | |0 P:(DE-82)IDM02007 |a Schupp, Stefan |b 0 |u rwth |
| 245 | _ | _ | |a State set representations and their usage in the reachability analysis of hybrid systems |c vorgelegt von Stefan Alexander Schupp, Master of Science |h online |
| 246 | _ | 3 | |a Zustandsmengenrepräsentierungen und ihre Verwendung in der Erreichbarkeitsanalyse Hybrider Systeme |y German |
| 260 | _ | _ | |a Aachen |c 2019 |
| 300 | _ | _ | |a 1 Online-Ressource (217 Seiten) : Illustrationen, Diagramme |
| 336 | 7 | _ | |0 2 |2 EndNote |a Thesis |
| 336 | 7 | _ | |0 PUB:(DE-HGF)11 |2 PUB:(DE-HGF) |a Dissertation / PhD Thesis |b phd |m phd |
| 336 | 7 | _ | |2 BibTeX |a PHDTHESIS |
| 336 | 7 | _ | |2 DRIVER |a doctoralThesis |
| 336 | 7 | _ | |2 DataCite |a Output Types/Dissertation |
| 336 | 7 | _ | |2 ORCID |a DISSERTATION |
| 500 | _ | _ | |a Veröffentlicht auf dem Publikationsserver der RWTH Aachen University |
| 502 | _ | _ | |a Dissertation, RWTH Aachen University, 2019 |b Dissertation |c RWTH Aachen University |d 2019 |g Fak01 |o 2019-09-25 |
| 520 | 3 | _ | |a Unter hybriden Systemen in der Informatik versteht man Systeme, welche diskretes als auch kontinuierliches Verhalten vereinen. In dieser Arbeit werden Ergebnisse aus dem Bereich der Verifikation linearer hybrider Systeme vorgestellt. Das kontinuierliche Verhalten der betrachteten Systeme kann dabei durch lineare Differentialgleichungen beschrieben werden. Diese Arbeit beschäftigt sich im Besonderen mit der über-approximierenden Erreichbarkeitsanalyse, in der die Menge der erreichbaren Zustände durch eine endliche Vereinigung von Zustandsmengen approximiert wird. Zustandsmengen während der Berechnung werden dabei durch verschiedene geometrische als auch symbolische Repräsentierungen dargestellt. Die Wahl der Zustandsmengenrepräsentierung hat einen starken Einfluss auf die Präzision der Approximation als auch auf die Laufzeit der Analyse. Zusätzlich wird das Ergebnis der Analyse durch weitere Parameter und Heuristiken beeinflusst. In dieser Arbeit erforschen wir den Einfluss und die optimale Einstellung dieser Parameter. Unsere Ergebnisse sind in der öffentlichen C++ Bibliothek HyPro zur Verfügung gestellt. Die Beiträge dieser Arbeit lassen sich in drei Teile gliedern: 1) Wir präsentieren unsere HyPro Programmierbibliothek. Diese beinhaltet Implementierungen verschiedener Datentypen, die in Algorithmen für die Erreichbarkeitsanalyse hybrider Systeme verwendet werden können um Zustandsmengen hybrider Systeme zu repräsentieren. Eine vereinheitlichte Schnittstelle zusammen mit Reduktions- und Konvertierungsmethoden erlauben die schnelle Implementierung von flexiblen Analysemethoden für lineare hybride Systeme. 2) Wir zeigen die Anwendbarkeit der Methoden und Datenstrukturen in HyPro anhand der Einbettung eines üblichen Erreichbarkeitsanalyseansatzes in ein Framework, in welchem eine schnelle aber grobe Analyse iterativ durch die Verwendung von Gegenbeispielen verfeinert wird. Eine Parallelisierung des Ansatzes ist ebenfalls gegeben, welche die Laufzeiten weiter verbessert. 3) Die Einführung von Methoden, um teure Berechnungen in hoch-dimensionalen Zustandsräumen durch weniger aufwendigen Berechnungen in niedrig-dimensionalen Zustandsräumen zu ersetzen. Die vorgestellte Methode ist nur unter bestimmten Bedingungen verwendbar. Wir präsentieren ein automatisiertes Verfahren, um diese Bedingungen zu überprüfen und wenn möglich solche niedrig-dimensionale Räume zu identifizieren. Die Verwendung dedizierter Verfahren für die Analyse bestimmter Unterklassen von hybriden Systemen in Kombination mit der Entkopplung des Zustandsraumes vervollständigen unseren Ansatz. |l ger |
| 520 | _ | _ | |a Hybrid systems in computer science are systems with combined discrete-continuous behavior. This work presents results obtained in the field of safety verification for linear hybrid systems whose continuous behavior can be described by linear differential equations. We focus on a special technique named flowpipe-construction-based reachability analysis, which over-approximates the reachable states of a given hybrid system as a finite union of state sets. In these computations we can use different geometric and symbolic representations for state sets as datatypes. The choice of the state set representation has a strong impact on the precision of the approximation and on the running time of the analysis method. Additionally, numerous further parameters and heuristics influence the analysis outcome. In this work we investigate on the influence and optimal usage of these parameters. Our results are collected in a publicly available open-source C++ programming library named HyPro. The major contributions of this work are threefold: 1) We present our HyPro library offering implementations for several state set representations that are commonly used in flowpipe-construction-based reachability analysis. A unified interface in combination with reduction and conversion methods supports the fast implementation of versatile analysis methods for linear hybrid systems. 2) We put our library to practice and show its applicability by embedding a flowpipe-construction-based reachability analysis method in a CEGAR-based abstraction refinement framework. The parallelization of this approach further increases its performance. 3) We introduce methods to decompose the search space and replace high-dimensional computations by computations in lower-dimensional subspaces. This method is applicable under certain conditions. An automated check of these conditions, an automated decomposition, and the integration of dedicated analysis methods for subspace computations extend our approach. |l eng |
| 588 | _ | _ | |a Dataset connected to Lobid/HBZ |
| 591 | _ | _ | |a Germany |
| 653 | _ | 7 | |a formal methods |
| 653 | _ | 7 | |a hybrid systems |
| 653 | _ | 7 | |a reachability analysis |
| 653 | _ | 7 | |a safety verification |
| 700 | 1 | _ | |0 P:(DE-82)IDM00047 |a Ábrahám, Erika |b 1 |e Thesis advisor |u rwth |
| 700 | 1 | _ | |0 P:(DE-82)150288 |a Frehse, Goran |b 2 |e Thesis advisor |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/767529/files/767529.pdf |y OpenAccess |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/767529/files/767529_source.zip |y Restricted |
| 909 | C | O | |o oai:publications.rwth-aachen.de:767529 |p VDB |p dnbdelivery |p driver |p open_access |p openaire |
| 910 | 1 | _ | |0 I:(DE-588b)36225-6 |6 P:(DE-82)IDM02007 |a RWTH Aachen |b 0 |k RWTH |
| 910 | 1 | _ | |0 I:(DE-588b)36225-6 |6 P:(DE-82)IDM00047 |a RWTH Aachen |b 1 |k RWTH |
| 914 | 1 | _ | |y 2019 |
| 915 | _ | _ | |a OpenAccess |0 StatID:(DE-HGF)0510 |2 StatID |
| 920 | 1 | _ | |0 I:(DE-82)121310_20140620 |k 121310 |l Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) |x 0 |
| 920 | 1 | _ | |0 I:(DE-82)120000_20140620 |k 120000 |l Fachgruppe Informatik |x 1 |
| 920 | 1 | _ | |0 I:(DE-82)080060_20170720 |k 080060 |l Graduiertenkolleg UnRAVeL |x 2 |
| 980 | _ | _ | |a I:(DE-82)120000_20140620 |
| 980 | _ | _ | |a I:(DE-82)121310_20140620 |
| 980 | _ | _ | |a UNRESTRICTED |
| 980 | _ | _ | |a VDB |
| 980 | _ | _ | |a phd |
| 980 | _ | _ | |a I:(DE-82)080060_20170720 |
| 980 | 1 | _ | |a FullTexts |
| Library | Collection | CLSMajor | CLSMinor | Language | Author |
|---|