Model checking is an efficient formal method for the verification of hardware and software designs. Based on model checking, VTT offers a service for verifying that automation system software design fulfils stated requirements. The difference to more common verification methods (like testing or simulation) is that all the possible executions of the system model are taken into account. Exhaustive analysis means that hidden design errors can be found in systems that have already undergone verification through conventional means.
An exhaustive formal verification method
Testing and simulation are proven and valuable verification methods, but considering the number of different inputs and internal variables that a typical automation function has, exhaustive analysis (100% test coverage) is often impossible. How, then, can we make sure that everything will work out fine in all possible situations?
Model checking is a formal, computer-assisted verification method, where a software tool called a model checker is used to prove that a system model satisfies stated (functional) properties. The system is typically modelled as a finite-state machine, and temporal logic is used for property formalisation. The analysis is remarkably fast.
If a model execution contrary to a property is found, it is then returned as a counterexample. Review of the counterexample can then reveal a design error in the system (or an error in the way the system model or the properties were formulated, which can then be corrected).
Model checking therefore completely avoids the issue of having to specify test cases or input scenarios. All execution paths relevant to each specified property are covered, leading to 100% coverage without having to individually consider all possible model states.
Automation software verification service
VTT provides an automation software verification service based on model checking. The objective of the work can be hunting for potential design errors, or comprehensive, independent verification (to support, e.g., system safety justification). In the latter case, VTT will produce a verification report identifying the method and the tools used in the analysis, the target system, the documents used in constructing the model, and the requirements that were verified.
The target is typically an automation software design specification, expressed using graphical languages such as function block diagrams, state diagrams, sequential function charts, etc. With extra work, it is also possible to consider different failure modes of the underlying hardware architecture.
Property specification is based on requirement specifications, or other functional descriptions. If suitable documents do not exists, or the available documentation is incomplete, VTT can help collect the verifiable properties by, e.g., interviewing people involved in the design.
VTT uses graphical tools for model checking of function block diagrams. The counterexamples can be visualised as a 2D animation, useful for highlighting potential design issues.
Potential findings are reported using visualisations based on the format of the original design sheets. A typical finding is a clear-cut scenario that violates a stated requirement. It is then up to the customer to consider the relevance of the problem and the need for modifications.
Case example: Automation renewal at the Loviisa nuclear power plant
Photo: Fortum
In the early 2000s, Fortum started preparing the automation renewal project (LARA) of the nuclear power plant in Loviisa. New systems were to be delivered by a consortium of AREVA and Siemens. Within LARA, VTT has provided an independent, third-party automation software verification service based on model checking. Verification has covered automation functions of several safety-classified LARA subsystems, including reactor protection, preventive protection, and emergency diesel generator functions.
In Fortum’s view, model checking has proved to be a rigorous method for verifying complex I&C functions. The key benefit is exhaustive verification, covering all possible input signal sequences. This means that also events occurring within very small time windows can be analysed, which is challenging when using more traditional verification methods. Furthermore, the mere act of constructing the model (using the precision required by the method) can reveal errors and inconsistencies in design documentation that are easily missed upon manual review. [source]
In May 2014, Forum decided to discontinue the LARA project due to delays in the project implementation, and signed an agreement with Rolls-Royce regarding modernisation. In 2016, VTT provided model checking services in the context of the new project (ELSA).
Reference projects
The list of practical customer projects VTT has carried out includes, but is not limited to:
 |
|
 |
|
 |
|
In research projects, VTT has also successfully applied model checking for the verification of machine and factory automation systems.