Model Checking-Based Application-Dependent Quantitive Metrics to Drive the Fault Probability for the Discrete State System

Abstract

Risk evaluation needs the probability of faults, and two common approaches for accomplishing it are gathering statistics from
existing systems or relying on the experience of experts. In cases where we develop a novel system, none of these approaches
is feasible. This paper proposes an application-dependent method to drive a quantitative metric that can yield fault probability
for risk analysis. This method applies to discrete state-based systems. We model a system via formal methods like colored
Petri nets and then generate the state-space graph of the system via the CPN tool. The state-space graph contains complete
information about the states of the system, and we can prove some of the system's properties via model checking. Model
checking permits us to define application/system-specific values that give feasible metrics to assign the probability value for
a fault. A warehouse guard movement strategy is considered a case study, and we proposed a colored Petri net model of the
system. A metric from model checking of the state-space graph is derived to assign the probability of the intruder's success in
infiltrating the warehouse.