Integration of Petri Nets into STAMP / CAST on the example of Wenzhou 7.23 accident

This paper illustrates how formal models, in this case Petri nets, can be integrated into the promising STAMP approach. CENELEC 5012X recommend applying formal methods to demonstrate safety in the railway sector. STAMP does not include formal modeling and therefore seems inadequate for safety analysis in railway traffic. This drawback can be eliminated by hybridizing the approach with the ProFunD hazard analysis (DIN EN 62551) using Petri net models. Such a new method, called formalSTAMP that successfully integrates a formal model into STAMP is introduced in this paper. A sample accident analysis application on the Wenzhou 7.23 accident in China is performed and the results are presented in contrast to an original STAMP / CAST analysis by (Dong 2012).