Automation and Verification of Safety-critical Systems

|

Selected publications from my group and of close research associates and partners

Formal verification of nuclear instrumentation and control systems

Modelling of Instrumentation and Control Logic

  1. Pakonen, A., Biswas, P., & Papakonstantinou, N. (2020). Transformation of non-standard nuclear I&C logic drawings to formal verification models. In IECON 2020 : 46th Annual Conference of the IEEE Industrial Electronics Society (pp. 697-704). IEEE Institute of Electrical and Electronic Engineers. https://doi.org/10.1109/iecon43393.2020.9255176 [web]

Requirements

  1. Buzhinsky I. Formalization of natural language requirements into temporal logics: a survey. 17th IEEE International Conference on Industrial Informatics (INDIN). July 22–25, 2019, Helsinki-Espoo, Finland, pp. 400–406. IEEE, 2019 [web] [preprint] [slides]
  2. Pakonen A., Pang C., Buzhinsky I., Vyatkin V. User-friendly formal specification languages – conclusions drawn from industrial experience on model checking. IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2016), Berlin, Germany, September 6–9, 2016, pp. 1–8 [web] [preprint]

Model-checking

  1. Buzhinsky I., Pakonen A. Symmetry breaking in model checking of fault-tolerant nuclear instrumentation and control systems. IEEE Access, vol. 8, 2020, pp. 197684–197694. DOI: 10.1109/ACCESS.2020.3034799 [pdf] [web] [tool]
  2. Pakonen A., Buzhinsky I., Björkman K. Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems. Reliability Engineering & System Safety, Volume 205, January 2021, 107237 [pdf] [web]
  3. Buzhinsky I., Pakonen A. Timed model checking of fault-tolerant nuclear I&C systems. 18th IEEE International Conference on Industrial Informatics (INDIN 2020). July 20–23, 2020, Warwick, UK, pp. 159–164. IEEE, 2020 [preprint] [slides]
  4. Pakonen A., Buzhinsky I. Verification of fault tolerant safety I&C systems using model checking. 20th IEEE International Conference on Industrial Technology (ICIT), February 13–15, 2019, Melbourne, Australia, pp. 969–974. IEEE, 2019 [web] [preprint] [slides]
  5. Buzhinsky I., Pakonen A., Vyatkin V. Synthesis-aided reliability assurance of basic block models for model checking purposes. 27th IEEE International Symposium on Industrial Electronics (ISIE). June 13–15, 2018, Cairns, Australia, pp. 669–674. IEEE, 2018 [web] [preprint] [slides] [tool]
  6. Buzhinsky I., Pakonen A., Vyatkin V. Explicit-state and symbolic model checking of nuclear I&C systems: A comparison. 43rd Annual Conference of the IEEE Industrial Electronics Society (IECON). October 29 – November 01, Beijing, China, pp. 5439–5446. IEEE, 2017 [web] [preprint] [slides]
  7. Buzhinsky I., Pakonen A. Model-checking detailed fault-tolerant nuclear power plant safety functions. IEEE Access, vol. 7, 2019, pp. 162139–162156. DOI: 10.1109/ACCESS.2019.2951938 [pdf] [web] [tool]
  8. Pakonen, A., & Björkman, K. (2017). Model checking as a protective method against spurious actuation of industrial control systems. In M. Cepin, & R. Briš (Eds.), Safety and Reliability: Theory and Applications (pp. 3189-3196). CRC Press. https://doi.org/10.1201/9781315210469 [web]

Analysis of model-checking results

  1. Pakonen A., Buzhinsky I., Vyatkin V. Counterexample visualization and explanation for function block diagrams. 16th IEEE International Conference on Industrial Informatics (INDIN). July 18–20, 2018, Porto, Portugal, pp. 747–753. IEEE, 2018 [web] [preprint] [slides] [tool]
  2. Ovsiannikova P., Buzhinsky I., Pakonen A., Vyatkin V. Oeritte: user-friendly counterexample explanation for model checking. IEEE Access, 2021. DOI: 10.1109/ACCESS.2021.3073459 [pdf] [web] [tool]
  3. P. Ovsiannikova, V. Vyatkin, Towards user-friendly model checking of IEC 61499 systems with counterexample explanation, Proceedings of the 26th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2021, Wästerås, Sweden, IEEE [pdf]

Use of IEC 61499 for implementation of safety-critical automation systems

  1. A. George, P. Ovsiannikova, V. Vyatkin, Towards unambiguous FBD: IEC 61499 modelling, automatic generation and equivalence testing, IEEE International Symposium on Industrial Electronics (ISIE’21), June 2021, Kyoto, Japan [pdf] [video presentation]

Formal verification of IEC 61499 function blocks

  1. M. Xavier, S. Patil, V. Vyatkin, Cyber-physical automation systems modelling with IEC 61499 for their formal verification, IEEE International conference on Industrial Informatics (INDIN’21), Palma de Mallorca, Spain, July, 2021 [web]
  2. V. Shatrov, V. Vyatkin, Promela Formal Modelling and Verification of IEC61499 Systems with comparison to SMV, IEEE International conference on Industrial Informatics (INDIN’21), Palma de Mallorca, Spain, July, 2021 [pdf]
  3. Drozdov, D., Dubinin, V., Patil, S. and Vyatkin, V., 2021. A Formal Model of IEC 61499-Based Industrial Automation Architecture Supporting Time-Aware Computations. IEEE Open Journal of the Industrial Electronics Society, 2, pp.169-183 [pdf]

Monitors in IEC 61499 engineering

  1. P Jhunjhunwala, JO Blech, A Zoitl, UD Atmojo, V Vyatkin, A Design Pattern for Monitoring Adapter Connections in IEC 61499, 22nd IEEE International Conference on Industrial Technology (ICIT), 2021 [pdf]

Formal Synthesis and Correct-by-design of Distributed Automation Logic

  1. K.Chukharev, D. Suvorov, D. Chivilikhin, V.Vyatkin, “SAT-based Counterexample-Guided Inductive Synthesis of Distributed Controllers”, IEEE Access, 2020 [web]
  2. Zhou, N., Li, D., Vyatkin, V., Dubinin, V. and Liu, C., 2020. Toward Dependable Model-Driven Design of Low-Level Industrial Automation Control Systems. IEEE Transactions on Automation Science and Engineering [pdf]