Formal model-based quantitative safety analysis using timed Coloured Petri Nets

Fault Tree Analysis (FTA) and Event Tree Analysis (ETA) are by far the most frequently used qualitative and quantitative approaches in system reliability and safety analysis such as in the railway domain. FTA and ETA explain the causalities and consequences of hazards or accidents (e.g., rail traffic accidents) in terms of linear event sequences, which are difficult to incorporate none-linear relationships such as feedback. For quantitative analysis, FTA and ETA have disadvantages in dealing with dependent failure events. The quality assurance for fault trees and events trees is mainly carried out by peer review. In addition, traditional FTA and ETA are usually applied to systems that consists of non-repairable components. For systems that comprise repairable components, Markov models are widely used, which suffer however intensively from the state space explosion. Considering all these issues, we propose a formal model-based approach for quantitative safety analysis using timed Coloured Petri Nets (CPNs). There are three main contributions in this paper: firstly, a modelling method based on the specifications of timed message sequence charts, systems theory and decision tables for system components is raised for establishing timed hierarchical CPN models of systems that are appropriate for quantitative safety analysis. Secondly, state-space-based methods by exploring standard state space reports, and applying standard as well as non-standard queries to state spaces are presented to verify the untimed CPN models. Finally, methods of evaluating the safety characteristics of mean time to hazardous event and the probability of keeping in normal and safe states on the basis of the data collected during the simulation of the timed CPN models are provided. To illustrate our approach, a case study of a railway level crossing control system is presented as a running example throughout the paper.