Mahdi, Ahmed (2017) Advancing software model-checking by SMT interpolation beyond decidable arithmetic theories : an approach to verify safety properties in embedded and hybrid system models. PhD, Universität Oldenburg.

Preview

Volltext (5Mb)

Abstract

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.

["eprint_fieldname_abstract_plus" not defined]

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.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	Model-checking, SMT-interpolation, dead code detection, (probabilistic) reachability, model-slicing
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	11 Jan 2018 12:17
Last Modified:	12 Jan 2018 09:20
URI:	https://oops.uni-oldenburg.de/id/eprint/3445
URN:	urn:nbn:de:gbv:715-oops-35265
DOI:
Nutzungslizenz:

Actions (login required)

View Item