VERIFICATION OF AN INDUSTRIAL SAFETY FUNCTION USING COLOURED PETRI NETS AND MODEL CHECKING
Tamás Bartha, András Vörös, Attila Jámbor, Dániel Darvas · SZTAKI Publication Repository (Hungarian Academy of Sciences) · 2012
The verification of embedded, safety-critical industrial systems is important, since a failure of these systems may have catastrophic consequences.Formal methods guarantee not only the correctness, but also the completeness of the analysis.However, even moderately complex industrial systems have state spaces so large that former analysis techniques could not handle.In this paper we model and analyse a small, but important part of a safety-critical industrial system: a safety function initiating an emergency procedure in a nuclear power plant.We model safety function using a proprietary coloured Petri net formalism, and perform the analysis by symbolic model checking based on the saturation algorithm.The analysis results were computed by the model checking tool developed at our department * .Although this particular safety function has been analysed in earlier research [11], this is the first time the full behaviour of this system could be examined without any restrictions.