h1

000767529 001__ 767529
000767529 005__ 20241028133739.0
000767529 0247_ $$2HBZ$$aHT020212073
000767529 0247_ $$2Laufende Nummer$$a38567
000767529 0247_ $$2datacite_doi$$a10.18154/RWTH-2019-08875
000767529 037__ $$aRWTH-2019-08875
000767529 041__ $$aEnglish
000767529 082__ $$a004
000767529 1001_ $$0P:(DE-82)IDM02007$$aSchupp, Stefan$$b0$$urwth
000767529 245__ $$aState set representations and their usage in the reachability analysis of hybrid systems$$cvorgelegt von Stefan Alexander Schupp, Master of Science$$honline
000767529 246_3 $$aZustandsmengenrepräsentierungen und ihre Verwendung in der Erreichbarkeitsanalyse Hybrider Systeme$$yGerman
000767529 260__ $$aAachen$$c2019
000767529 300__ $$a1 Online-Ressource (217 Seiten) : Illustrationen, Diagramme
000767529 3367_ $$02$$2EndNote$$aThesis
000767529 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000767529 3367_ $$2BibTeX$$aPHDTHESIS
000767529 3367_ $$2DRIVER$$adoctoralThesis
000767529 3367_ $$2DataCite$$aOutput Types/Dissertation
000767529 3367_ $$2ORCID$$aDISSERTATION
000767529 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University
000767529 502__ $$aDissertation, RWTH Aachen University, 2019$$bDissertation$$cRWTH Aachen University$$d2019$$gFak01$$o2019-09-25
000767529 5203_ $$aUnter 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.$$lger
000767529 520__ $$aHybrid 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.$$leng
000767529 588__ $$aDataset connected to Lobid/HBZ
000767529 591__ $$aGermany
000767529 653_7 $$aformal methods
000767529 653_7 $$ahybrid systems
000767529 653_7 $$areachability analysis
000767529 653_7 $$asafety verification
000767529 7001_ $$0P:(DE-82)IDM00047$$aÁbrahám, Erika$$b1$$eThesis advisor$$urwth
000767529 7001_ $$0P:(DE-82)150288$$aFrehse, Goran$$b2$$eThesis advisor
000767529 8564_ $$uhttps://publications.rwth-aachen.de/record/767529/files/767529.pdf$$yOpenAccess
000767529 8564_ $$uhttps://publications.rwth-aachen.de/record/767529/files/767529_source.zip$$yRestricted
000767529 909CO $$ooai:publications.rwth-aachen.de:767529$$popenaire$$popen_access$$pdriver$$pdnbdelivery$$pVDB
000767529 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM02007$$aRWTH Aachen$$b0$$kRWTH
000767529 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00047$$aRWTH Aachen$$b1$$kRWTH
000767529 9141_ $$y2019
000767529 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000767529 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation)$$x0
000767529 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
000767529 9201_ $$0I:(DE-82)080060_20170720$$k080060$$lGraduiertenkolleg UnRAVeL$$x2
000767529 961__ $$c2019-10-17T13:18:24.637411$$x2019-09-29T20:43:13.703207$$z2019-10-17T13:18:24.637411
000767529 980__ $$aI:(DE-82)120000_20140620
000767529 980__ $$aI:(DE-82)121310_20140620
000767529 980__ $$aUNRESTRICTED
000767529 980__ $$aVDB
000767529 980__ $$aphd
000767529 980__ $$aI:(DE-82)080060_20170720
000767529 9801_ $$aFullTexts