Advancing software model-checking by SMT interpolation beyond decidable arithmetic theories : an approach to verify safety properties in embedded and hybrid system models
Sie können Bookmarks mittels Listen verwalten, loggen Sie sich dafür bitte in Ihr SLUB Benutzerkonto ein.
Medientyp:
E-Book;
Elektronische 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
Beteiligte:
Mahdi, Ahmed
[VerfasserIn]
Erschienen:
Carl von Ossietzky Universität Oldenburg: /oops/ - Oldenburger Online-Publikations-Server, 2017
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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.