MODEL CHECKING REVEALS HIDDEN ERRORS IN SAFETY-CRITICAL IC SOFTWARE

摘要

Function blocks are a common programming language for safety-classified instrumentation and control (I&C) systems. While designs of elementary function blocks can be proven error-free through rigorous component and unit testing procedures, verification and validation of complex function block diagrams might only be based on inspections and reviews. Arguments for error-free software are often supported by claiming high quality in software development practices and referring to operational experience. Model checking is an efficient formal method for the verification of (hardware or software) system designs. A model checker is a software tool that checks that a model of a system satisfies given requirements in all possible situations. The difference to more traditional V&V methods, such as testing and simulation, is that the analysis is exhaustive - covering all possible executions. We have been studying the use of model checking for verifying nuclear power plant software design in several research projects. The method has also been adopted into practical use; as an example, we have been consulting the Finnish Radiation and Nuclear Safety Authority (STUK) on evaluating NPP I&C system designs using model checking since 2008. In this paper, we present a method for model checking of function block based systems. Since model checking also requires the formal specification of system requirements, we also present a method for requirement specification based on requirement templates.