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