Introduction of the case study
The subject of our research is a safety function, designed to initiate an emergency prevention action in the occurrence of the so-called PRISE event. This safety function is used in the Paks Nuclear Power Plant (Paks NPP) located in Hungary. Nuclear power plants are highly safety-critical and complex systems, where the correct operation of the safety procedures is of great importance. The plant protection systems must satisfy high safety requirements and minimize spurious forced outages. Therefore, formal modelling and verification methods need to be applied to prove the correctness and completeness of the PRISE safety function.