Boolean-logic driven Markov processes : Explained. Analysed. Verified.

Khan, Shahid; Stoelinga, Mariëlle Ida Antoinette; Katoen, Joost-Pieter

doi:10.18154/RWTH-2022-09528

Boolean-logic driven Markov processes : Explained. Analysed. Verified. = Durch Boolesche Logik gesteuerte Markov-Prozesse – Erklärt. Analysiert. Verifiziert.

Khan, Shahid^RWTH*

2022

Verantwortlichkeitsangabevorgelegt von Shahid Khan, M.Sc.

ImpressumAachen : RWTH Aachen University 2022

Umfang1 Online-Ressource : Illustrationen, Diagramme

ReiheAachener Informatik-Berichte (AIB) ; 2022,02

Dissertation, RWTH Aachen University, 2022

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Stoelinga, Mariëlle Ida Antoinette (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2022-10-04

Online
DOI: 10.18154/RWTH-2022-09528
URL: https://publications.rwth-aachen.de/record/854417/files/854417.pdf

Einrichtungen

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Modellbasierte Zuverlässigkeitsstudien von technischen Systemen laufen auf die Quantifizierung und Verbesserung von Zuverlässigkeitsmaßen hinaus. Diese Maßnahmen umfassen Zuverlässigkeit, Verfügbarkeit, Wartbarkeit und Sicherheit. Zwei Hauptbestandteile solcher Studien sind 1) Modelle, die das Systemverhalten auf einem akzeptablen Abstraktionsniveau erfassen, und 2) effiziente und genaue Analysetechniken zur Quantifizierung von Zuverlässigkeitsmaßen .Unter den Modellierungstechniken sind statische (oder Standard-)Fehlerbäume (SFTs) eine herausragende Zuverlässigkeitsmodellierungssprache, die von Ingenieuren ausgiebig verwendet wird, um Systemmodelle zu entwickeln. Es fehlt jedoch an Aussagekraft, da es zeitliche Abhängigkeiten von Ausfällen nicht modellieren kann und Reparaturen nur begrenzt unterstützt. Boolesche logikgesteuerte Markov-Prozesse (BDMP) und dynamische Fehlerbäume (DFT) sind zwei klassische dynamische Erweiterungen von SFTs, die darauf abzielen, die Probleme der Ausdrucksleistungsbegrenzung von SFTs zu mildern. Während DFTs (im Allgemeinen) auf nicht reparierbare Systeme beschränkt sind, unterstützen BDMPs nativ Reparaturen. Die BDMP-Sprache hat eine lange Geschichte der industriellen Nutzung; Das führende französische Elektrizitätsversorgungsunternehmen (EDF) verwendet BDMPs ausgiebig, um Zuverlässigkeitsstudien durchzuführen. Unter den Analysetechniken ist die probabilistische Modellprüfung eine Verifikationstechnik zur Bestimmung der Wahrscheinlichkeit, dass ein Zustandsraummodell eine logische Eigenschaft erfüllt oder widerlegt. Es kombiniert effiziente, vollautomatische Verifikationsalgorithmen mit numerischer Analyse. Die Ergebnisse dieser automatisierten Überprüfungsverfahren sind numerische Werte, die Zuverlässigkeitspraktiker verwenden, um das Zuverlässigkeitswachstum ihrer Systeme zu erreichen. Das Problem mit BDMPs ist, dass ihnen eine numerisch exakte Analyseunterstützung und eine angemessen dokumentierte Semantik fehlen. EDF bietet zwei Analysewerkzeuge für BDMPs: 1) einen Monte-Carlo-Simulator und 2) ein Sequenzexplorationswerkzeug. Beide Tools liefern ungefähre Ergebnisse, die für strenge Anforderungen an die Zuverlässigkeit sicherheitskritischer Systeme möglicherweise nicht akzeptabel sind. Die Semantik von BDMPs ist wesentlich für eine vergleichende Studie mit anderen Modellierungssprachen, z. B. DFTs. Diese Dissertation, die in Zusammenarbeit mit EDF entwickelt wurde, stellt Semantik und einen Model Checker für BDMPs vor:-- wir schlagen Markov-Automaten- und verallgemeinerte stochastische Petrinetz-basierte Semantik für BDMPs vor und stellen empirisch die Genauigkeit fest,-- wir entwickeln einen probabilistischen Modellprüfer für BDMPs und verbessern die Skalierbarkeit des Modellprüfers unter Verwendung von Teilzustands-Weltraumexplorationstechniken, und-- wir stellen BDMPs DFTs gegenüber und erheben das reparierbare Verhalten von BDMPs zu reparierbaren DFTs. Diese Dissertation bietet eine ganzheitliche Sicht auf BDMPs. Ein spannendes Ergebnis dieser Dissertation ist, dass unser Modellprüfer die markovische Teilmenge der von EDF gepflegten Figaro-Sprache analysieren kann. Diese Teilmenge umfasst Kapazitätsanalysediagramme, dynamische Zuverlässigkeitsblockdiagramme, elektrische Schaltungen, Petrinetze, Prozessdiagramme, Telekommunikationsnetzwerke und andere von EDF entwickelte Figaro-basierte Modellierungsformalismen.

Model-based dependability studies of engineering systems amount to quantifying and improving dependability measures. These measures include reliability, availability, maintainability and safety. Two key ingredients of such studies are 1) models capturing the system behaviour to an acceptable level of abstraction and 2) efficient and accurate analysis techniques to quantify dependability measures. Among the modelling techniques, static (or standard) fault trees (SFTs) is a prominent dependability modelling language extensively used by engineers to develop system models. However, it lacks expressive power as it cannot model temporal dependencies of failures and has limited support for repairs. Boolean logic-driven Markov processes (BDMPs) and dynamic fault trees (DFTs) are two classical dynamic extensions of SFTs that aim to mitigate the expressive power limitation issue of SFTs. While DFTs are (generally) restricted to non-repairable systems, BDMPs natively support repairs. The BDMP language has a long-standing industrial usage history; the leading French electricity utility company (EDF) extensively uses BDMPs to conduct dependability~studies. Among the analysis techniques, probabilistic model checking is a verification technique to determine the probability of a state-space model satisfying or refuting a logical property. It combines efficient, fully automated verification algorithms with numerical analysis. The results of these automated verification procedures are numeric values that dependability practitioners use to attain the reliability growth of their systems. The issue with BDMPs is that it lacks numerically exact analysis support and adequately documented semantics. EDF provides two analysis tools for BDMPs: 1) a Monte-Carlo simulator and 2) a sequence exploration tool. Both tools provide approximate results, which may not be acceptable for stringent dependability requirements of safety-critical systems. The semantics of BDMPs is essential for a comparative study with other modelling languages, e.g., DFTs. This dissertation, developed in collaboration with EDF, presents semantics and a model checker for BDMPs:-- we propose Markov automaton- and generalised stochastic Petri net-based semantics to BDMPs and empirically establish the accuracy,-- we develop a probabilistic model checker for BDMPs and enhance the scalability of the model checker using partial state-space exploration techniques, and-- we contrast BDMPs to DFTs and lift the repairable behaviour of BDMPs to repairable DFTs. This dissertation provides a holistic view of BDMPs. An exciting outcome of this dissertation is that our model checker can analyse the Markovian subset of the EDF-maintained Figaro language. This subset includes capacity analysis diagrams, dynamic reliability block diagrams, electric circuits, Petri nets, process diagrams, telecommunication networks, and other EDF-developed Figaro-based modelling formalisms.

OpenAccess:
PDF
(additional files)