Causality Checking of Safety-Critical Software and Systems

Lade...
Vorschaubild
Dateien
Leitner_0-286535.pdf
Leitner_0-286535.pdfGröße: 4.13 MBDownloads: 825
Datum
2015
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
DOI (zitierfähiger Link)
ArXiv-ID
Internationale Patentnummer
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Gesperrt bis
Titel in einer weiteren Sprache
Publikationstyp
Dissertation
Publikationsstatus
Published
Erschienen in
Zusammenfassung

The complexity of modern safety-critical systems is steadily increasing due to the amount of functionality that is implemented in those systems.In order to be able to asses the correctness and safety of these systems in a comprehensive manner automated or, at least, computer-aided techniques are needed.
Model checking, a formal verification technique, provides an automated algorithmic analysis of system models and is able to check whether a formalized requirement is satisfied by the system. If the requirement is violated the model checker provides error traces, called counterexamples, which serve as witnesses for the requirement violation. While the counterexamples can be used as a debugging aid, they do not provide any obvious insight into which events are causal for the requirement violation. In order to derive the causal events from a set of counterexamples, the events of all error traces need to be manually inspected, which is an error prone and time consuming task.

We propose a method complementing model checking that is called causality checking. Causality checking algorithmically computes the causal events for the violation of a requirement that is formalized as a non-reachability property. The notion of causality that we use is based on the actual cause definition by Halpern and Pearl, which in turn is based on the counterfactual argument by Lewis. Causality checking is able to compute the causal events for a property violation and also takes the order in which the events appear into account as a causal factor. Furthermore, causality checking identifies the causal non-occurrence of events. We propose a causality checking algorithm and show how it can be integrated into the state-space exploration algorithms used in qualitative model checking.

The hardware of an embedded system may fail due to deterioration and affect the software that is running on this hardware and thereby cause a requirement violation. In industry negative exponentially distributed rates are used in order to specify the occurrence probability of such a hardware failure in a given time frame. In order to support a probabilistic analysis of the system we extend the causality checking approach to be applicable to probabilistic system models. The proposed probabilistic causality checking approach enables us to compute the probabilities of certain combinations of events that cause a property violation. A pure probabilistic causality checking method, as will become clear in this thesis, entails a high performance penalty for the necessary probabilistic counterexample computation. We will show how this bottleneck can be mitigated by a combination of qualitative and probabilistic causality checking.

While a full state-space exploration of the case studies that we analyze is possible, we discuss the implications of an incomplete state-space exploration of the analysis model with respect to soundness and completeness of the causality checking result and present strategies that can be applied in order to increase the scalability of the causality checking approach.

Furthermore, we discuss how the causality checking method can be integrated into the QuantUM framework, a method that allows for the generation of the analysis models from higher-level architectural description languages such as the unified modeling language (UML) or the systems modeling language (SysML). For the result representation we propose a temporal logic called event order logic which allows for a concise and formal representation of the causal events and the causal orderings. Furthermore, we show how formulas in event order logic, that have been computed by the causality checker, can be represented by fault trees, a method used in industry to reason about causal relationships between property violations and events. The mapping to fault trees facilitates the interpretation of the causality checking results and is a representation that is already known and used in industry.

We demonstrate the applicability and usefulness of the causality checking approach on several case studies from industry and academia and discuss how causality checking can be used in an industrial safety engineering process.

Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
causality, model checking, verification
Konferenz
Rezension
undefined / . - undefined, undefined
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Datensätze
Zitieren
ISO 690LEITNER-FISCHER, Florian, 2015. Causality Checking of Safety-Critical Software and Systems [Dissertation]. Konstanz: University of Konstanz
BibTex
@phdthesis{LeitnerFischer2015Causa-30778,
  year={2015},
  title={Causality Checking of Safety-Critical Software and Systems},
  author={Leitner-Fischer, Florian},
  address={Konstanz},
  school={Universität Konstanz}
}
RDF
<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/30778">
    <dcterms:issued>2015</dcterms:issued>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2015-04-17T07:59:02Z</dc:date>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/30778/3/Leitner_0-286535.pdf"/>
    <dc:language>eng</dc:language>
    <dc:contributor>Leitner-Fischer, Florian</dc:contributor>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:title>Causality Checking of Safety-Critical Software and Systems</dcterms:title>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dcterms:abstract xml:lang="eng">The complexity of modern safety-critical systems is steadily increasing due to the amount of functionality that is implemented in those systems.In order to be able to asses the correctness and safety of these systems in a comprehensive manner automated or, at least, computer-aided techniques are needed.&lt;br /&gt;Model checking, a formal verification technique, provides an automated algorithmic analysis of system models and is able to check whether a formalized requirement is satisfied by the system. If the requirement is violated the model checker provides error traces, called counterexamples, which serve as witnesses for the requirement violation. While the counterexamples can be used as a debugging aid, they do not provide any obvious insight into which events are causal for the requirement violation. In order to derive the causal events from a set of counterexamples, the events of all error traces need to be manually inspected, which is an error prone and time consuming task.&lt;br /&gt;&lt;br /&gt;We propose a method complementing model checking that is called causality checking. Causality checking algorithmically computes the causal events for the violation of a requirement that is formalized as a non-reachability property. The notion of causality that we use is based on the actual cause definition by Halpern and Pearl, which in turn is based on the counterfactual argument by Lewis. Causality checking is able to compute the causal events for a property violation and also takes the order in which the events appear into account as a causal factor. Furthermore, causality checking identifies the causal non-occurrence of events. We propose a causality checking algorithm and show how it can be integrated into the state-space exploration algorithms used in qualitative model checking.&lt;br /&gt;&lt;br /&gt;The hardware of an embedded system may fail due to deterioration and affect the software that is running on this hardware and thereby cause a requirement violation. In industry negative exponentially distributed rates are used in order to specify the occurrence probability of such a hardware failure in a given time frame. In order to support a probabilistic analysis of the system we extend the causality checking approach to be applicable to probabilistic system models. The proposed probabilistic causality checking approach enables us to compute the probabilities of certain combinations of events that cause a property violation. A pure probabilistic causality checking method, as will become clear in this thesis, entails a high performance penalty for the necessary probabilistic counterexample computation. We will show how this bottleneck can be mitigated by a combination of qualitative and probabilistic causality checking.&lt;br /&gt;&lt;br /&gt;While a full state-space exploration of the case studies that we analyze is possible, we discuss the implications of an incomplete state-space exploration of the analysis model with respect to soundness and completeness of the causality checking result and present strategies that can be applied in order to increase the scalability of the causality checking approach.&lt;br /&gt;&lt;br /&gt;Furthermore, we discuss how the causality checking method can be integrated into the QuantUM framework, a method that allows for the generation of the analysis models from higher-level architectural description languages such as the unified modeling language (UML) or the systems modeling language (SysML). For the result representation we propose a temporal logic called event order logic which allows for a concise and formal representation of the causal events and the causal orderings. Furthermore, we show how formulas in event order logic, that have been computed by the causality checker, can be represented by fault trees, a method used in industry to reason about causal relationships between property violations and events. The mapping to fault trees facilitates the interpretation of the causality checking results and is a representation that is already known and used in industry.&lt;br /&gt;&lt;br /&gt;We demonstrate the applicability and usefulness of the causality checking approach on several case studies from industry and academia and discuss how causality checking can be used in an industrial safety engineering process.</dcterms:abstract>
    <dc:rights>terms-of-use</dc:rights>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2015-04-17T07:59:02Z</dcterms:available>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/30778"/>
    <dc:creator>Leitner-Fischer, Florian</dc:creator>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/30778/3/Leitner_0-286535.pdf"/>
  </rdf:Description>
</rdf:RDF>
Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Kontakt
URL der Originalveröffentl.
Prüfdatum der URL
Prüfungsdatum der Dissertation
March 6, 2015
Hochschulschriftenvermerk
Konstanz, Univ., Diss., 2015
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
Begutachtet
Diese Publikation teilen