Sign In

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 counter examples 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.

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

​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.

​Since 2008, VTT has applied model checking in practical customer projects in the Finnish nuclear industry.
More information on the practical customer projects can be found in the SimulationStore website.


 

​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/

 

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

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 +3 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 +3 time zone