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

• Durch Boolesche Logik gesteuerte Markov-Prozesse - Erklärt. Analysiert. Verifiziert

Khan, Shahid; Katoen, Joost-Pieter (Thesis advisor); Stoelinga, Mariëlle Ida Antoinette (Thesis advisor)

Aachen : RWTH Aachen University (2022)
Buch, Doktorarbeit

In: Aachener Informatik-Berichte (AIB) AIB-2022-02
Seite(n)/Artikel-Nr.: 1 Online-Ressource : Illustrationen, Diagramme

Dissertation, RWTH Aachen University, 2022

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.