Is your automation system fail-safe? VTT Model checking reveals hard-to-detect I&C logic design issues that can potentially cause damage to production assets, loss of production and even danger to people and the environment. VTT has a decade of experience in the verification of nuclear industry systems. Our team is able to ensure the reliability and usability of safety or cost critical systems on various domains, e.g. railway, aviation, infrastructure or chemical industry.
Key facts
Model checking helps you prevent disasters, both in terms of safety and profit.
The analysis is 100% exhaustive against the stated requirements. If a scenario that will breach the requirement is possible, model checking will find it.
Already a well-established practice in Finnish nuclear industry!
Design review is one of the essential phases in the engineering of safety-critical systems, where experts analyse what can potentially go wrong with the system, such as events that could cause the system to give conflicting actuation commands. Model checking is an efficient formal method of verification of hardware and software designs. The method verifies the system model against formal properties, based on functional requirements.
When model checking is carried out as part of the system delivery project, detected flaws can be corrected well before commissioning. The method can also be applied to systems already in use to improve safety and operational efficiency.
The difference compared to common verification methods (such as testing or simulation) is that model checking takes all relevant executions of the system model into account. No test case planning is needed; instead, the method automatically identifies ‘counter-example’ scenarios in which the system will breach its requirements. Through this exhaustive analysis, hidden design errors can be uncovered in systems that have already undergone verification through conventional means.
The results are so remarkable, that we will order similar verification also for functions with lower safety classification. Thankfully we can purchase services like these from VTT!
Practical projects in the nuclear sector
VTT has a decade of experience in model checking, including system verification of Finnish nuclear power plants:
Olkiluoto 3 is an EPR type reactor under commissioning. Since 2008, on commission from the Finnish regulator STUK, VTT has evaluated the plant’s software-based Protection System and FPGA-based Priority and Actuator Control System.
Fortum operates two VVER-440 type reactors in Loviisa, Finland. In the I&C modernization project ELSA, VTT has performed independent, third-party reviews of seven different systems. Based on the results, design modifications have been made to the Reactor Trip System and the Reactor Power Control System.
Hanhikivi 1 is a NPP new build planned in Pyhäjoki, Finland. On commission from the utility Fennovoima, VTT has evaluated the functional architecture, detecting design issues that could cause, e.g., spurious actuation, contradictory commands, or otherwise incorrect response.
Design errors caught early in the design phase
Results in the energy sector are excellent, with several hidden errors in safety-critical systems successfully discovered.
In Fortum's view, model checking is seen as truly beneficial in nuclear I&C projects. With formal verification, more deficiencies can be found already during the design phase.
Model checking can be applied in any industry where automation functionality is expressed in logic programming language (function block, ladder, or sequence diagrams) or hardware description language (e.g. VHDL).
We have utilised VTT's model checking as one method at Mipro to ensure the safety of the interlocking device. The method is well suited for locating design errors and has helped us to improve railway safety.
