% IMPORTANT: The following is UTF-8 encoded. This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.
@PHDTHESIS{Khan:854417,
author = {Khan, Shahid},
othercontributors = {Katoen, Joost-Pieter and Stoelinga, Mariëlle Ida
Antoinette},
title = {{B}oolean-logic driven {M}arkov processes : {E}xplained.
{A}nalysed. {V}erified.},
volume = {2022,02},
school = {RWTH Aachen University},
type = {Dissertation},
address = {Aachen},
publisher = {RWTH Aachen University},
reportid = {RWTH-2022-09528},
series = {Aachener Informatik-Berichte (AIB)},
pages = {1 Online-Ressource : Illustrationen, Diagramme},
year = {2022},
note = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
University; Dissertation, RWTH Aachen University, 2022},
abstract = {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.},
cin = {121310 / 120000},
ddc = {004},
cid = {$I:(DE-82)121310_20140620$ / $I:(DE-82)120000_20140620$},
typ = {PUB:(DE-HGF)11 / PUB:(DE-HGF)3},
doi = {10.18154/RWTH-2022-09528},
url = {https://publications.rwth-aachen.de/record/854417},
}
guest ::