Formal Verification of Function Block Diagram based Specifications for the I&C

Function Block Diagrams (FBDs) are a widely used specification method in modern I&C systems used in the development of safety-critical software. The need for the integration of automated formal verification in the development process in order to increase software reliability is constantly increasing. This paper presents a Coloured Petri net based approach to the formal verification of Function Block Diagram based specifications. The approach is non model based; only the control logic of the safety function is modeled and verified. The proof of required properties is based on reachability analysis and model checking. The objective of the work is to demonstrate the possibility of integrating the formal analysis into the control software development process of a nuclear power plant (NPP).