Model checking of automation systems

Exhaustive verification of system design

Model checking is a computer-aided verification method developed to formally verify the correct functioning of a system design model against its formal specification. Typically, some variant of state machines are used to model the system, while the specifications are formalized with temporal logics.

Model checking tools use efficient algorithms to verify whether all the behaviours of the system model satisfy the system specification. In case the specification is violated, the model checking tools create counterexamples describing executions of the system model that are violating the property.

In several research and customer projects, VTT has found model checking an efficient method for supplementing e.g. safety analyses of instrumentation and control (I&C) systems in nuclear power plants. The exhaustiveness of the analysis means that design issues can be identified in systems that have already undergone verification using more conventional means (e.g., testing, simulations, reviews…).

Research at VTT has focused on industry-specific challenges, covering topics such as:

  • Integration of model checking with requirement engineering, simulation-assisted testing, probabilistic reliability assessment, etc.
  • Verification of large and complex systems
  • User-friendly formal property specification languages

Verification service & tool development

Based on ten years of practical industry experience, VTT also provides a I&C verification service based on model checking. Our customers include the Finnish nuclear regulator STUK, as well as the nuclear power companies Fortum and Fennovoima (see the "References" tab).

Over the years we have identified tens of design issues (see the "Examples" tab).

VTT is also developing practical tools for the verification of industrial control software (see the "Tools" tab). MODCHK is a modelling tool that provides a graphical user interface for modelling function block diagrams and animating counterexample traces. Still in development, MODCHK is already used in-house, both for customer projects and research purposes.

​Since 2008, VTT has applied model checking in practical customer projects in the Finnish nuclear industry.

For practical examples of identified design issues, see the "Examples" tab.

 

fortum_logo.png

 

Independent, third-party verification of nuclear I&C application software design

Customer: Fortum Power and Heat, a utility operating two NPPs in Loviisa, Finland.

Fortum operates two VVER-440 type reactors that started operation in 1977 and 1980. The old instrumentation and control systems are being replaced with modern, digital I&C supplied by Rolls-Royce. In the modernization project (ELSA), VTT has performed independent, third-party review of selected I&C functions of the:

  • Reactor Trip System (RTS)
  • Reactor Power Control System (RPCS)
  • Reactor Power Limitation System (RPLS)
  • Preventive Actuation and Indication System (PAIS)
  • Preventive Protection System (PPS)
  • Neutron Flux Measurement System (NFS)
  • Manual Backup System (MBS) - functional design
     

Based on VTT's analysis results, design modifications have been made to RPCS and RTS.

For the analysis on PPS, VTT also verified how the Rolls-Royce's Spinline based systems operate together with already installed systems developed by another vendor.

"In Fortum's view, model checking is seen truly beneficial in nuclear I&C projects. [...] With formal verification, more deficiencies can be found already during the design phase. [...] The obvious benefit of model checking is that through exhaustive analysis, it is possible to find very rare transitional states that occur during a short period of time." [full quote]

 

stuk_logo.png

 

Verification of  I&C application software and FPGA application logic design

Customer: Radiation and Nuclear Safety Authority (STUK), the Finnish nuclear regulator

Olkiluoto 3 is a European Pressurised Water Reactor (EPR) under construction by Areva. Since 2008, VTT has evaluated OL3 I&C systems on commission from the Finnish regulator STUK. The analysis has covered selected safety functions of:

  • Protection System (PS)
  • Priority and Actuator Control System (PACS)
     

Both PS and PACS are based on Areva's Teleperm XS technology.

PACS is based on Field-Programmable Gate Array (FPGA) technology, consisting of two diverse modules: SPLM1-PC11 and AV42. VTT verified the application logic of both components in isolation, and also verified how the two FPGA based components operate together with the software based Protection System to perform, e.g., periodic tests.

​"Model checking is a very effective method to evaluate complex I&C functions and find design defects that may not be practically possible to find in field test of plant simulator [...] Even when defects do not have direct safety significance, they may give a good impression on the quality of system development processes." [full quote]

 

fennovoima_logo.png

 

Verification of a functional I&C architecture

Customer: Fennovoima, a utility with a decision-in-principle for a NPP in Pyhäjoki, Finland

Hanhikivi 1 is a NPP planned to be built in Pyhäjoki, Finland. The utility Fennovoima has submitted a construction license application for a AES-2006 type pressurised water reactor.

On commission from Fennovoima, VTT has evaluated preliminary versions of the Hanhikivi 1 functional architecture. The functional architecture defines and describes the safety functions of the plant in an early design stage. In the later stages to follow, the functional architecture is then used a as input for the actual I&C system design. High quality of the functional architecture is therefore essential, since changes in the later life-cycle phases could cause significant delays for the project.

The analysis focused on the safety functions that were considered mode complex than others (due to use of, e.g., memory function blocks, delay function blocks, or feedback loops.

"The use of formal methods like model checking is planned to have a role in the assessment of the Hanhikivi 1 functional architecture. Fennovoima also expects that model checking will be used to assess the eventual detailed design of safety classified I&C functions, where applicable." [full quote]

We've collected data on the design issues identified in our practical customer projects between 2008 and 2016 (see the "References" tab). Here, a design issue means that model checking revealed a practical example of a potential scenario, where the I&C application logic ends up in a state that is contrary to a stated functional requirement.

A full list of the 40 identified issues can be found in this paper. 

Based on the data, we can see that:

  • 37% of the identified design issues were related to spurious actuation scenarios, where the I&C logic inadvertently actuates the function, without real demand. Our experience therefore proves that spurious actuation can be tackled with model checking, and in fact, to the best of our knowledge, it is the only truly effective method available.
  • 42% of the issues involved very exact timing of external events, e.g., independent events occurring on the same processor cycle. Testing for such scenarios is very challenging.
  • 32% of the issues involved human user actions, typically personnel (operation or maintenance) doing something ill-advised or ill-timed.
  • 17% of the issues required the interaction between several systems for the problem to occur. Analysing the target system in isolation would not have revealed the issue.
  • 7% of the issues resulted in the process signal freezing permanently on some fixed state (requiring, e.g., system restart for recovery)
     

Since our analysis is often targeted at system designs that have already been analysed using more traditional means (e.g., testing, simulation or expert review), the identifies issues often deal with unexpected and unlikely situations.

Example: Operational mode selection logic

The figure below shows a modified and abstracted version of an application logic that we have verified, containing only the blocks that are necessary to reproduce the problematic scenario (the actual system model consisted of 74 function blocks and had an I/O number of 23). The logic has two functions: one for selecting the operational mode a, and another for selecting the mode b. The operator can use the set_a or set_b command to select the associated mode, and the selection is stored into a flip-flop memory block. It mode a is selected, and the signal c then becomes true, the mode is automatically changed to b. The processing order is made explicit by using a cycle delay block.

 

For the logic, we can identify requirements such as:

  • r1: "The set_a command shall lead to a, if b is not already selected",
    or as a formal LTL property p1: G((set_a ∧ ¬ b) → a).
  • r2: "The set_a command shall reset b, if c is not active",
    or p2: G((set_a ∧ ¬ c) → ¬ b).
  • r3: "The set_b command shall lead to b and reset a if set_a is not active",
    or p3: G((set_b ∧ ¬ set_a) → (b ∧ ¬ a)).
  • r4: "If a has been selected, the signal c shall change the selection to b",
    or p4: G((Yac) → b).
  • r5: "Only one mode (a or b) shall be active at the same time",
    or p5: G¬ (ab).
     

We can also specify properties that address spurious actuation, such as "a can only be selected if set_a has been active at some point", or: G(aO set_a).

Verification results indicate that p5 is false. The model checker returns a counterexample which is visualised in the figure below:

 

In the counterexample scenario, mode b is first selected, and the signal c is also on. The operator then activates the set_a command, which does not reset b, because c is still on. At the same time, c does not reset a because the cycle delay block is delaying the a signal. Finally, on the nect processing cyle, both set_a and c are reset at the exact same time, and both a and b remain set.

The issue depends on three factors that are unlikely and difficult to account for in test planning:

  1. The operator uses set_a while c is also true, which is not necessarily feasible.
  2. For some reason (e.g., device failure), the set_a signal pulse is extremely short.
  3. Two signals are reset at the exact same time (same processor cycle).

In model checking, the analyst need not worry with coming up with such scenarios. It suffices to state the property that a and b shall not be on at the same time, exhaustive analysis takes care of the rest.

VTT has developed a graphical tool called MODCHK for verifying function block based application logic design. Based on a graphical model of a vendor-specific function block diagram and a set of formal properties, MODCHK generates the necessary input files for the NuSMV model checker. The counterexamples produced by NuSMV are visualised using 2D animation (see figure below).

 

Features of the tool include:

  • Manually specified elementary function block libraries, which is a necessity, since vendors (especially in the nuclear domain) use vendor-specific, non-standard, black-box blocks.
  • Elementary blocks can have internal property variables with predefined default values.
  • User-generated composite function blocks allowing for deep hierarchy.
  • Processing of signal validity, which is often used in nuclear I&C applications.
  • Counterexample animation using line colour and thickness for binary signals, numerical monitors for analogue signals, and dashed lines for invalid signals.
     

VTT is also working with Fortum on developing automatic translation of Apros I&C logic models to MODHCK.

Used in VTT's customer projects since 2014, MODCHK has made practical work more efficient than before. VTT and Fortum aim to eventually release MODCHK as a software product under the Apros product family.

A. Pakonen, T. Tahvonen, M. Hartikainen, M. Pihlanko, Practical applications of model checking in the Finnish nuclear industry, 10th International Topical Meeting on Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies (NPIC & HMIT 2017), 11 - 15 June, 2017, San Francisco, CA, USA, pp. 1342-1352.

A. Pakonen, K. Björkman, Model checking as a protective method against spurious actuation of industrial control systems, 27th European Safety and Reliability Conference (ESREL 2017), 18 - 22 June 2017, Portoroz, Slovenia, pp. 3189-3196.

A. Pakonen, C. Pang, I. Buzhinsky, V. Vyatkin, User-friendly formal specification languages - conclusions drawn from industrial experience on model checking, 21th IEEE Conference on Emerging Technologies and Factory Automation (ETFA 2016), 6 - 9 September 2016, Berlin, Germany. IEEE (2016)

J. Lahtinen, T. Kuismin, K. Heljanko, Verifying large modular systems using iterative abstraction refinement, Reliability engineering and system safety. Elsevier. Vol. 139 (2015), 120-130.

A. Pakonen, J. Valkonen, S. Matinaho, M. Hartikainen, Model Checking for Licensing Support in the Finnish Nuclear Industry, International Symposium on Future I&C for Nuclear Power Plants (ISOFIC 2014), Jeju Island, Repulic of Korea, 24 - 28 August 2014. Korean Nuclear Society (2014)

J. Lahtinen, Verification of fault-tolerant system architectures using model checking, 1st International Workshop on Development, Verification and Validation of Critical Systems (DEVVARTS), Lecture Notes in Computer Science, Vol. 8696, p. 195 – 206, Springer, September 2014.

A. Pakonen, T. Mätäsniemi, J. Lahtinen, T. Karhela, A Toolset for Model Checking of PLC Software, 18th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA2013, 10-13 September 2013, Cagliari, Italy, Proceedings. IEEE (2013)

J. Lahtinen, J. Valkonen, K. Björkman, J. Frits, I. Niemelä, K. Heljanko, Model checking of safety critical software in the nuclear engineering domain, Reliability Engineering and System Safety. Elsevier. Vol. 105 (2012) No: Special Issue ESREL 2010, 104 – 113

J. Lahtinen, K. Björkman, J. Valkonen, I. Niemelä, Emergency diesel generator control system verification by model checking and compositional minimization, 8th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2012), Znojmo, Czech Republic, 25 - 28 October 2012, Proceedings. Czech Republic (2012), 49 – 60

J. Lahtinen, Automatic test set generation for function block based systems using model checking, 9th International Conference on the Quality of Information and Communications Technology (QUATIC 2014), Guimarães, Portugal, p. 216 – 225, IEEE, September 2014.

K. Björkman, J. Valkonen, J. Ranta, Verification of Automated Changeover Switching Unit by Model Checking, Proceedings of the 7th International Topical Meeting on Nuclear Plant Instrumentation, Control and Human-Machine Interface Technologies(NPIC&HMIT 2010), November 7-11, 2010, Las Vegas, Nevada, 1719-1728

J. Valkonen, K. Björkman, J. Frits, I. Niemelä, Model checking methodology for verification of safety logics, SIAS 2010 - The 6th International Conference on Safety of Industrial Automated Systems. Tampere, 14.-15.6.2010, SIAS 2010 Proceedings. Suomen Automaatioseura (2010), 6 p.

K. Björkman, J. Frits, J. Valkonen, J. Lahtinen, K. Heljanko, I. Niemelä and J.J. Hämäläinen, Verification of Safety Logic Designs by Model Checking, Sixth American Nuclear Society International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies, NPIC&HMIT 2009, Knoxville, Tennessee, April 5-9, 2009, on CD-ROM, American Nuclear Society, LaGrange Park, IL 2009.

J. Valkonen, M. Koskimies, V. Pettersson, K. Heljanko, J.-E. Holmberg, I. Niemelä, and J. J. Hämäläinen, Formal verification of safety I&C system designs: Two nuclear power plant related applications, Enlarged Halden Programme Group Meeting - Proceedings of the Man-Technology-Organisation Sessions, C4.2., Institutt for Energiteknikk, Halden, Norway, 2008.

J. Valkonen, V. Pettersson, K. Björkman, J.-E. Holmberg, M. Koskimies, K. Heljanko, and I. Niemelä, Model-Based Analysis of an Arc Protection and an Emergency Cooling System - MODSAFE 2007 Work Report. VTT Working Papers 93, VTT Technical Research Centre of Finland, Espoo, Finland, February 2008, 51 p.

​​Integrated Safety Assessment and Justification of Nuclear Power Plant Automation (SAUNA)

The general objective of SAUNA (2015-2018) is to develop an integrated framework for safety assessment and transparent safety demonstration of nuclear power plant instrumentation and control (I&C) systems. Part of the project is dedicated to developing methods and tools for assessing the safety of systems and their development processes. For model checking, in particular, research topics include closed-loop modelling of industrial processes, user-friendly property specification, and integration with other tools and methods such as probabilistic reliability assessment or structure-based testing.


SAFIR2018 programme website: http://safir2018.vtt.fi/

 

CONTACT US

P.O. Box 1000, FI-02044 VTT, Finland
Tel. exchange +358 20 722 111
Opening hours Mon - Fri 8:00 - 16:30,
UTC +2 time zone

CUSTOMER SERVICE

info@vtt.fi
Tel. +358 20 722 7070
Opening hours Mon - Fri 9:00 - 11:00 and 12:00 - 15:00,
UTC +2 time zone