+**********************************************************************
*
*
* 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