Safety analysis using coloured Petri nets

The authors propose a safety analysis method using coloured Petri nets (CPN). Their method employs a backward approach where a hazard is assumed to have occurred and backward simulation from the hazard is performed in order to determine if and how the hazard might occur. Using CPN, they define a hazard as a set of markings and perform backward simulation by generating a reachability graph backwards from the hazard. To facilitate the safety analysis, they extend the semantics of CPN and define backward reachability graphs of CPN. To demonstrate their method, a shutdown system for a Korean nuclear power plant is used as an example