Sie können Bookmarks mittels Listen verwalten, loggen Sie sich dafür bitte in Ihr SLUB Benutzerkonto ein.
Medientyp:
E-Book;
Hochschulschrift
Titel:
Advancing software model-checking by SMT interpolation beyond decidable arithmetic theories
:
an approach to verify safety properties in embedded and hybrid system models
Hochschulschrift:
Dissertation, Carl von Ossietzky Universität Oldenburg, 2017
Dissertation, Oldenburg, Universität Oldenburg, 2017
Anmerkungen:
Beschreibung:
Die Überprüfung der Erreichbarkeit kontrollorientierter Softwaresysteme wird komplexer, wenn sie arithmetische und probabilistische Hybridmodelle umfassen. Das Erkennen nichterreichbarer Codesegmente eines Programms (sog. tote Codes) ist in verschiedenen Standards für die Entwicklung eingebetteter Systeme erforderlich. Die meisten früheren Arbeiten können nicht mit Programmen umgehen, die nichtlineare Arithmetik induzieren. Diese Einschränkung wurde durch die Kombination mehrerer Techniken überwunden, welche die Zustandsraumexplosion angehen und große arithmetische Randbedingungen lösen. Eine Variante dieser Technik würde die probabilistische Erreichbarkeit durch Berechnen der maximalen Wahrscheinlichkeit des Erreichens schlechter Zustände in einem probabilistischen Modell verifizieren. Schließlich wird ein Modell-Slicing-Ansatz eingeführt, um Assumption-Commitment-Eigenschaften in Rechenmodellen zu verifizieren, die eine konsistente Semantik des Übergangssystems induzieren. <dt.>
Verifying reachability of control-oriented software systems is an industrial quest which is becoming more complex to answer when programs involve arithmetic and probabilistic hybrid models. Whenever code segments of a program are unreachable, they are called dead codes. Detecting dead code is required in various standards for embedded system development. Most previous work can’t handle programs inducing non-linear arithmetic, as they are confined to linear programs. This restriction was overcome by combining several techniques that attack state space explosion and solve large arithmetic constraints system. Additionally, a variant of this technique would verify probabilistic reachability by computing the maximum probability of reaching bad states in a probabilistic model. Finally, a model-slicing approach is introduced to verify assumption-commitment properties in computational models which induce consistent transition system semantics. <engl.>