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

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.