Practical solutions for the model-checking of fault-tolerant instrumentation and control system logics

Thumbnail Image

Files

isbn9789526426471.pdf (2.46 MB)

URL

Journal Title

Journal ISSN

Volume Title

School of Electrical Engineering | Doctoral thesis (article-based) | Defence date: 2025-08-15
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.

Authors

Date

2025

Department

Sähkötekniikan ja automaation laitos
Department of Electrical Engineering and Automation

Major/Subject

Mcode

Degree programme

Language

en

Pages

131 + app. 76

Series

Aalto University publication series Doctoral Theses, 139/2025

Abstract

Software in industrial instrumentation and control (I&C) systems is subject to high reliability requirements. If human errors made in I&C software engineering cause control failures during operation, the outcome, depending on the application, could be a huge financial loss, a severe hazard to health or the environment, or even loss of life. Modern digital I&C systems are complex and so full of intricate dependencies that traditional met of proving their safety and reliability fall short. Model checking is a formal, computerassisted verification method, that can be used to logically prove that a model of the system is correct. The method has been proven to find hidden errors in designs already subjected to rigorous testing. VTT has used the method in Finnish nuclear and rail traffic industry projects and found over a hundred design issues. Still, the broader application of model checking has been hampered by thelack of user-friendly, domain-specific tools. This thesis examines ways of (1) making the work process of I&C logic model checking more userfriendly, accessible, and cost-effective, and (2) broadening the scope in which I&C design can be analysed. First, it presents a tool-supported approach for modelling and analysing fault-tolerant I&C logics used in, e.g., nuclear facilities. Second, it examines ways of accounting for the failure modes of the underlying I&C hardware, when verifying that the logics are fault-tolerant. Third, it shows how infinite-state modelling and compositional verification can be applied to logics where the more common approach of symbolic, discrete-state model checking falls short. The practical applicability of the contribution has been proven by evaluating the developed methods against data and models collected from real industrial projects and employing the methods in practice. The new techniques explored in the thesis, now already in used in VTT’s projects, have already uncovered design issues in logics that were previously thought too complex to check.

Modernit, ohjelmistopohjaiset automaatiojärjestelmät ovat niin monimutkaisia ja täynnä riippuvuuksia, etteivät perinteiset menetelmät niiden todentamiseen enää riitä. Mallintarkastus on formaali, tietokoneavusteinen todennusmenetelmä, jonka avulla voidaan loogisesti todistaa, että järjestelmästä tehty malli täyttää annetut vaatimukset. Menetelmän avulla on käytännössä löytynyt piileviä virheitä järjestelmistä senkin jälkeen, kun niitä on perusteellisesti testattu. VTT on soveltanut mallintarkastusta suomalaisissa ydinvoima- ja raideliikennehankkeissa, ja havaintoja on tehty jo yli sata. Mallintarkastuksen laajempaa käyttöä kuitenkin vaikeuttaa helppokäyttöisten ja automaatioohjelmistoille räätälöityjen työkalujen puute. Tässä työssä on tutkittu keinoja (1) tehdä automaatio-ohjelmistojen mallintarkastuksesta helpompaa, käytännöllisempää ja halvempaa, sekä (2) löytää uusia keinoja soveltaa mallintarkastusta entistä laajemmin. Työssä esitetään työkaluavusteinen menetelmä vikasietoiseksi rakennettujen automaatio-ohjelmistojen mallinnukseen ja analyysiin. Lisäksi tutkitaan keinoja huomioida ohjelmiston tarkastuksessa automaatiolaitteiden vikaantumistapoja. Lopuksi vielä näytetään, kuinka reaalilukumatematiikkaan perustuvia algoritmeja ja osissa todentamisen menetelmiä voidaan soveltaa niihin malleihin, joita laajemmin käytetyt (äärellisiin tilakoneisiin ja symboliseen todennukseen perustuvat) mallintarkastimet eivät pysty käsittelemään. Työssä kehitettyjen menetelmien soveltuvuus käytäntöön on todennettu arvioimalla niitä teollisista hankkeista kerättyjä dataa ja malleja vasten, sekä soveltamalla niitä teollisissa projekteissa. Työssä tutkitut uudet tekniikat on jo otettu käyttöön VTT:n projekteissa, ja niiden avulla on jo paljastunut suunnitteluvirheitä malleissa, joita aiemmin käytetyillä tekniikoilla ei ollut mahdollista tarkistaa.

Description

Supervising professor

Vyatkin, Valeriy, Prof., Aalto University, Department of Electrical Engineering and Automation, Finland

Thesis advisor

Kortelainen, Juha, Dr., VTT, Finland

Keywords

instrumentation and control system, application software, model checking, formal methods, verification, fault tolerance, automaatiojärjestelmä, sovellusohjelmisto, mallintarkastus, formaalit menetelmät, todennus, vikasietoisuus

Other note

Parts

  • [Publication 1]: Antti Pakonen, Igor Buzhinsky, and Kim Björkman. Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems. Reliability Engineering & System Safety, vol. 205, 107237, Jan. 2021.
    Full text in Acris/Aaltodoc: https://urn.fi/URN:NBN:fi:aalto-202010165850
    DOI: 10.1016/j.ress.2020.107237 View at publisher
  • [Publication 2]: Antti Pakonen, Igor Buzhinsky, and Valeriy Vyatkin. Evaluation of visual property specification languages based on practical model-checking experience. Journal of Systems and Software, vol. 216, 112153, Oct. 2024.
    Full text in Acris/Aaltodoc: https://urn.fi/URN:NBN:fi:aalto-202408095380
    DOI: 10.1016/j.jss.2024.112153 View at publisher
  • [Publication 3]: Antti Pakonen and Igor Buzhinsky. Verification of fault tolerant safety I&C systems using model checking. In 20th IEEE International Conference on Industrial Technology (ICIT), Melbourne, Australia, pp. 969–974, Feb. 2019.
    DOI: 10.1109/ICIT.2019.8755014 View at publisher
  • [Publication 4]: Antti Pakonen, Igor Buzhinsky, and Valeriy Vyatkin. Counterexample visualization and explanation for function block diagrams. In 16th International Conference on Industrial Informatics (INDIN), Porto, Portugal, pp. 747–753, July 2018.
    DOI: 10.1109/INDIN.2018.8472025 View at publisher
  • [Publication 5]: Antti Pakonen. Model-checking infinite-state nuclear safety I&C systems with nuXvm. In 19th IEEE International Conference on Industrial Informatics (INDIN), Palma de Mallorca, Spain, July 2021.
    DOI: 10.1109/INDIN45523.2021.9557445 View at publisher
  • [Publication 6]: Antti Pakonen. Compositional verification of nuclear safety I&C systems with OCRA. In 29th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), Padova, Italy, Sept. 2024.
    DOI: 10.1109/ETFA61755.2024.10711009 View at publisher

Citation

Permanent link to this item

https://urn.fi/URN:ISBN:978-952-64-2647-1

Collections

[diss] Sähkötekniikan korkeakoulu / ELEC