Abstract
This paper presents the formal verification of a primary-to-secondary leaking (abbreviated as PRISE) safety procedure in a nuclear power plant (NPP). The software for the PRISE is defined by the Function Block Diagram specification method.
Our approach to the formal verification of the PRISE safety procedure is based on the coloured Petri net (CPN) representation. The CPN model of the checked software is derived by reinterpretation from the FBD diagram, using a pre-developed library of CPN subnets. This results in a high-level, hierarchical coloured Petri net, that has an almost identical structure to the FBD specification.
The state space of the CPN model was drastically reduced by “folding” equivalent states and trajectories into equivalence classes. Some of the safety properties could be proven based on the SCC (strongly connected components) graph of the reduced state space. Other properties were proven by CTL temporal logic based model checking.
This research has been supported by the Hungarian Scientific Research Fund through grant K67625, which is gratefully acknowledged.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Murata, T.: Petri Nets: Properties, Analysis and Application. Proceedings of the IEEE 77(4), 541–580 (1989)
Design/CPN – Computer Tool for Coloured Petri Nets, CPN group at the University of Aarhus, Denmark (2002), http://www.daimi.au.dk/designCPN/
Jensen, K.: Coloured Petri Nets – Basic Concepts, Analysis Methods and Practical Use. In: Basic Concepts. Monographs in Theoretical Computer Science, vol. 1. Springer, Heidelberg (1992)
Jensen, K.: Coloured Petri Nets – Basic Concepts, Analysis Methods and Practical Use. In: Analysis Methods. Monographs in Theoretical Computer Science, vol. 2. Springer, Heidelberg (1997)
Mertke, T., Menzel, T.: Methods and tools to the verification of safety-related control software. In: Proc. of the IEEE Int. Conf. on Sys., Man and Cybernetics (SMC 2000), Nashville, USA, pp. 2455–2457 (2000)
Younis, M.B., Frey, G.: Formalization of existing PLC programs: A survey. In: Proc. of the IEEE/IMACS Multiconf. on Comp. Eng. in Sys. App. (CESA 2003), Lille, France, Paper No. S2–R–00–0239 (2003)
Heiner, M.: Verification and optimization of control programs by Petri nets without state explosion. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 69–84. Springer, Heidelberg (1997)
Park, J.H., Seong, P.H.: An integrated knowledge base development tool for knowledge acquisition and verification for NPP dynamic alarm processing systems. Annals of Nuclear Energy 29, 447–463 (2002)
Son, H.S., Seong, P.H.: Development of a safety critical software requirements verification method with combined CPN and PVS: a nuclear power plant protection system application. Reliability Engineering and System Safety 80, 19–32 (2003)
Baresi, L., Mauri, M., et al.: PLCTools: Design, Formal Validation, and Code Generation for Programmable Controllers. In: Proc. of the IEEE Conf. on Sys., Man, and Cybernetics (SMC 2000), Nashville, USA, pp. 2437–2442 (2000)
Hanisch, H.M., Lobov, A., et al.: Formal Validation of Intelligent Automated Production Systems towards Industrial Applications. Int. J. of Manufacturing Tech. and Management 8(1), 75–106 (2006)
Wassyng, A., Lawford, M.: Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 133–153. Springer, Heidelberg (2003)
Lawford, M., Pantelic, V., Zhang, H.: Towards Integrated Verification of Timed Transition Models. Fundamenta Informaticae 70(1–2), 155–164 (2006)
International Standard IEC 61131-3: Programmable Controllers - Part 3: Programming Languages. International Electrotechnical Commission, Geneva, Switzerland (1993)
Minas, M., Frey, G.: Visual PLC-Programming using Signal Interpreted Petri Nets. In: Proc. of the American Control Conference 2002 (ACC 2002), Anchorage, Alaska, pp. 5019–5024 (2002)
Rossi, O., Schnoebelen, P.: Formal Modelling of Timed Function Blocks for the Automatic Verification of Ladder Diagram Programs. In: Proc. 4th Int. Conf. Automation of Mixed Processes: Hybrid Dynamic Systems (ADPM), Dortmund, Germany, pp. 177–182. Shaker Verlag, Germany (2000)
Németh, E., Bartha, T.: Formal verification of function block based specifications of safety-critical software. In: Modern Information Technology in the Innovation Processes of the Industrial Enterprises (MITIP 2006), Budapest, Hungary, pp. 211–218 (2006)
Németh, E., Fazekas, C., Szederkényi, G., Hangos, K.M.: Modeling and simulation of the primary circuit of the Paks nuclear power plant for control and diagnosis. In: Proceedings of the EUROSIM 2007, Ljubljana, Slovenia (2007) (on CD)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Németh, E., Bartha, T. (2009). Formal Verification of Safety Functions by Reinterpretation of Functional Block Based Specifications. In: Cofer, D., Fantechi, A. (eds) Formal Methods for Industrial Critical Systems. FMICS 2008. Lecture Notes in Computer Science, vol 5596. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03240-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-03240-0_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03239-4
Online ISBN: 978-3-642-03240-0
eBook Packages: Computer ScienceComputer Science (R0)