+**********************************************************************
*
*
*
Einladung
*
*
*
*
Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit:
Dienstag, 4. October 2022, 10:00 Uhr
Ort:
Raum 9222, Geb. E3, 2. Etage, Informatikzentrum, Ahornstr.
55
Referent:
Shahid Khan M.Sc.
(Lehrstuhl Informatik 2)
Thema:
Boolean-logic Driven Markov Processes - Explained. Analysed.
Verified.
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 safet-criticalsystems. 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.
In
this presentation, we provide: (1) a detailed introduction
to the BDMP formalism, (2) an insight of the
BDMP model checker, and (3) the semantics
of BDMPs.
Es
laden ein: die Dozentinnen und Dozenten der Informatik