Journal arcticles

  1. Pakonen A., Buzhinsky, I., Vyatkin, V. Evaluation of visual property specification languages based on practical model-checking experience.
    Journal of Systems and Software, vol. 216, October 2024, 112153.
    10.1016/j.jss.2024.112153 - cite
  2. Ovsiannikova, P., Pakonen A., Muromsky, D., Kobzev, M., Dubinin, V., Vyatkin, V. Formal verification on non-functional requirements of overall instrumentation and control architectures.
    IEEE Open Journal of the Industrial Electronics Society, vol. 5, June 2024, pp. 616 - 631.
    10.1109/OJIES.2024.3413568 - cite
  3. Ovsiannikova, P., Buzhinsky I., Pakonen A., Vyatkin V. Oeritte: user-friendly counterexample explanation for model checking.
    IEEE Access, vol. 9, 2021 pp. 61383-61397.
    10.1109/ACCESS.2021.3073459 - cite
  4. 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.
    10.1016/J.RESS.2020.107237 - cite
  5. 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.
    10.1109/ACCESS.2020.3034799 - cite
  6. Buzhinsky, I., Pakonen, A., Model-checking detailed fault-tolerant nuclear power plant safety functions.
    IEEE Access, vol. 7, 2019, pp. 162139-162156.
    10.1109/ACCESS.2019.2951938 - cite

Conference papers

  1. Pakonen, A., Tuominen, L., Viitasalo, M., Nuutinen, P. Formal Safety Assessment Methods in Olkiluoto 1&2 NPP I&C Renewal Project DIMA.
    14th Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2025), July 15-18, 2025, Chicago, IL, USA, pp. 1774-1783.
    10.13182/NPICHMIT25-46672 - cite
  2. Berger, J., King, A., Pakonen, A. Integrating STPA to NPP Systems Engineering Processes.
    14th Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2025), July 15-18, 2025, Chicago, IL, USA, pp. 1762-1771.
    10.13182/NPICHMIT25-46634 - cite
  3. Pakonen, A. Compositional verification of nuclear safety I&C systems with OCRA.
    29th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2024), September 10-13, 2024, Padova, Italy.
    10.1109/ETFA61755.2024.10711009 - cite
  4. Berger, J., Tiusanen, R., Kothalawala, H., Pakonen, A. Applying priority-informed STPA to a nuclear I&C system.
    29th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2024), September 10-13, 2024, Padova, Italy.
    10.1109/ETFA61755.2024.10710653 - cite
  5. Ovsiannikova, P., Pakonen, A., Vyatkin, V. Automatic generation of repair suggestions for control logic of I&C systems.
    49th Annual Conference of the IEEE Industrial Electronics Society (IECON 2023), October 16-19, 2023, Singapore.
    10.1109/IECON51785.2023.10311970 - cite
  6. Pakonen, A. Obfuscation of function block diagrams.
    28th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2023), September 12-15, 2023, Sinaia, Romania.
    10.1109/ETFA54631.2023.10275363 - cite
  7. Ovsiannikova, P., Pakonen, A., Vyatkin, V. Automatic generation of repair suggestions for overall I&C architecture represented with an ontology.
    28th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2023), September 12-15, 2023, Sinaia, Romania.
    10.1109/ETFA54631.2023.10275557 - cite
  8. Pakonen, A. Model-checking I&C logics — practical examples.
    13th Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2023), July 15-20, 2023, Knoxville, TN, USA, pp. 1610-1619.
    10.13182/NPICHMIT23-41122 - cite
  9. Björkman, K., Pakonen, A. Analyzing defense-in-depth properties of nuclear power plant instrumentation and control system architectures using ontologies.
    13th Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2023), July 15-20, 2023, Knoxville, TN, USA, pp. 1590-1599.
    10.13182/NPICHMIT23-41042 - cite
  10. Linnosmaa, J., Pakonen, A., Alanen, J. Demonstration of a model-based approach for formal verification of I&C logics.
    13th Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2023), July 15-20, 2023, Knoxville, TN, USA, pp. 1441-1450.
    10.13182/NPICHMIT23-41121 - cite
  11. Pakonen, A. Oops! Examples of I&C design issues detected with model checking.
    International Symposium on Future I&C for Nuclear Power Plants (ISOFIC 2021), November 15-17, 2021, Okoyama, Japan (hybrid online/offline event).
    cite
  12. Pakonen, A., Mätäsniemi, T. Ontology-based approach for analyzing nuclear overall I&C architectures.
    47th Annual Conference of the IEEE Industrial Electronics Society (IECON 2021), October 13-16, 2021, Toronto, Canada (held virtually).
    10.1109/IECON48115.2021.9589078 - cite
  13. Ovsiannikova, P., Pakonen, A., Vyatkin, V. Change-based causes in counterexample explanation for model checking.
    47th Annual Conference of the IEEE Industrial Electronics Society (IECON 2021), October 13-16, 2021, Toronto, Canada (held virtually).
    10.1109/IECON48115.2021.9589122 - cite
  14. Pakonen, A. Model-checking infinite-state nuclear safety I&C systems with nuXmv.
    19th IEEE International Conference on Industrial Informatics (INDIN 2021). July 21-23, 2021, Palma de Mallorca, Spain (held virtually).
    10.1109/INDIN45523.2021.9557445 - cite
  15. Pakonen, A. Model-checking of I&C logics — insights from over a decade of projects in Finland.
    12th ANS International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2021), June 14-17, 2021, Providence, RI, USA (held virtually), pp. 792-801.
    10.13182/T124-34322 - cite
  16. Ovsiannikova P., Buzhinsky I., Pakonen A., Vyatkin V. Visual counterexample explanation for model checking with Oeritte.
    25th International Conference on Engineering of Complex Computer Systems (ICECCS 2020), March 4-6, 2021, Singapore (held virtually), pp. 1-10.
    10.1109/ICECCS51672.2020.00008 - cite
  17. Pakonen, A., Biswas, P., Papakonstantinou, N. Transformation of non-standard nuclear I&C logic drawings to formal verification models.
    46th Annual Conference of the IEEE Industrial Electronics Society (IECON 2020), October 18-21, 2020, Singapore (held virtually), pp. 697-704.
    10.1109/IECON43393.2020.9255176 - cite
  18. Linnosmaa, J., Pakonen, A., Papakonstantinou, N., Karpati, P. Applicability of AADL in modelling the overall I&C architecture of a nuclear power plant.
    46th Annual Conference of the IEEE Industrial Electronics Society (IECON 2020), October 18-21, 2020, Singapore (held virtually), pp. 4337-4344.
    10.1109/IECON43393.2020.9254226 - cite
  19. 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 (held virtually), pp. 159-164.
    10.1109/INDIN45582.2020.9442188 - cite
  20. Pakonen, A., Buzhinsky, I. Verification of fault tolerant safety I&C systems using model checking.
    20th IEEE International Conference on Industrial Technology (ICIT 2019). February 13-15, 2019, Melbourne, Australia, pp. 969-974.
    10.1109/ICIT.2019.8755014 - cite
  21. Björkman, K., Pakonen, A. Coupling Model Checking and PSA: A Case Study.
    29th European Safety and Reliability Conference (ESREL 2019), September 22-26, 2019, Hannover, Germany, pp. 2789-2796.
    10.3850/978-981-11-2724-3_0418-cd - cite
  22. Pakonen, A., Buzhinsky, I., Vyatkin, V. Counterexample visualization and explanation for function block diagrams.
    16th International Conference on Industrial Informatics (INDIN 2018), July 18-20, 2018, Porto, Portugal, pp. 747-753.
    10.1109/INDIN.2018.8472025 - cite
  23. 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 2018), June 13-15, 2018, Cairns, Australia, pp. 669-674.
    10.1109/ISIE.2018.8433793 - cite
  24. Pakonen, A., Björkman, K. Model checking as a protective method against spurious actuation of industrial control systems.
    27th European Safety and Reliability Conference (ESREL 2017), June 18-22, 2017, Portoroz, Slovenia.
    cite
  25. Pakonen, A., Tahvonen, T., Hartikainen, M., Pihlanko, M. Practical applications of model checking in the Finnish nuclear industry.
    10th ANS International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2017), June 11-15, 2017, San Francisco, CA, USA, pp. 1342-1352.
    cite
  26. 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 2017), October 29 - November 1, 2017, Beijing, China, pp. 5439-5446.
    10.1109/IECON.2017.8216942 - cite
  27. Buzhinsky, I., Pakonen, A., Vyatkin, V. Scalable methods of discrete plant model generation for closed-loop model checking.
    43rd Annual Conference of the IEEE Industrial Electronics Society (IECON 2017), October 29 - November 1, 2017, Beijing, China, pp. 5483-5488.
    10.1109/IECON.2017.8216949 - cite
  28. Pakonen, A., Pang, C., Buzhinsky, I., Vyatkin, V. User-friendly formal specification languages — conclusions drawn from industrial experience on model checking.
    21st IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2016), September 6-9, 2016, Berlin, Germany.
    10.1109/ETFA.2016.7733717 - cite
  29. Pang, C., Pakonen, A., Buzhinsky, I., Vyatkin, V. A study on user-friendly formal specification languages for requirements formalization.
    14th IEEE International Conference on Industrial Informatics (INDIN 2016), July 19-21, 2016, Poitiers, France, pp. 676-682.
    10.1109/INDIN.2016.7819246 - cite
  30. Pakonen, A., Valkonen, J., Matinaho, S., Hartikainen. Model checking of I&C software in the Loviisa NPP automation renewal project.
    Automaatio XXI, March 15-18, 2015, Helsinki, Finland.
    cite
  31. Pakonen, A., Valkonen, J., Matinaho, S., Hartikainen, M. Model checking for licensing support in the Finnish nuclear industry.
    International Symposium on Future I&C for Nuclear Power Plants (ISOFIC 2014), August 24-28, 2014, Jeju Island, Republic of Korea.
    cite
  32. Pakonen, A., Mätäsniemi, T., Lahtinen, J., Karhela, T. A Toolset for model checking of PLC software.
    18th IEEE International Conference on Emerging Technologies & Factory Automation (ETFA 2013), September 10-13, 2013, Cagliary, Italy.
    10.1109/ETFA.2013.6648065 - cite
  33. Timonen, M., Pakonen, A., Tommila, T. Using associations and fuzzy ontologies for modeling chemical safety information.
    5th International Conference on Knowledge Engineering and Ontology Development (KEOD 2013), September 19-22, 2013, Algarve, Portugal, pp. 26-37.
    10.5220/0004536400260037 - cite
  34. Pakonen, A., Mätäsniemi, T., Valkonen, J. Model checking reveals hidden errors in safety-critical I&C software.
    8th ANS International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2012), July 22-26, 2012, San Diego, CA, USA.
    cite
  35. Pakonen, A., Tommila, T., Hirvonen, J. A fuzzy ontology based approach for mobilising industrial plant knowledge.
    15th IEEE International Conference on Emerging Technologies & Factory Automation (ETFA 2010), September 13-16, 2010, Bilbao, Spain.
    10.1109/ETFA.2010.5641200 - cite
  36. Hirvonen, J., Tommila, T., Pakonen, A., Carlsson, C., Fedrizzi, M., Fullér, R. Fuzzy keyword ontology for annotating and searching event reports.
    International Conference on Knowledge Engineering and Ontology Development (KEOD 2010), October 25-28, 2010, Valencia, Italy.
    10.5220/0003091002510256 - cite
  37. Pakonen, A., Lahtinen, J., Kuutti, V-P., Karhela, T. Integrating model checking with safety-critical I&C software design.
    7th ANS International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2010), November 7-11, 2010, Las Vegas, NV, USA, pp. 1729-1740.
    cite
  38. Pakonen, A., Pirttioja, T., Seilonen, I., Tommila, T. OWL based information agent services for process monitoring.
    12th IEEE International Conference on Emerging Technologies & Factory Automation (ETFA 2007), September 25-28, 2007, Patras, Greece, pp. 9-16.
    10.1109/EFTA.2007.4416747 - cite
  39. Pirttioja, T., Seilonen, I., Pakonen, A., Koskinen, K, Halme, A. Information agents handling semantic data as an extension to process monitoring systems.
    3rd International Conference on Industrial Applications of Holonic and Multi-Agent Systems (HoloMAS 2007), September 3-5, 2007, Regensburg, Germany, pp. 411-420.
    10.1007/978-3-540-74481-8_39 - cite
  40. Pakonen, A., Pirttioja, T., Seilonen, I., Tommila, T. Proactive computing in process monitoring: Information agents for operator support
    11th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2006), September 20-22, 2006, Prague, Czech Republic, pp. 153-158.
    10.1109/ETFA.2006.355408 - cite
  41. Seilonen, I., Pirttioja, T., Halme, A., Koskinen, K., Pakonen, A. Indirect process monitoring with constraint handling agents.
    4th IEEE International Conference on Industrial Informatics (INDIN 2006), August 16-18, 2006, Singapore, pp. 1323-1328.
    10.1109/INDIN.2006.275851 - cite
  42. Pirttioja, T., Pakonen, A., Seilonen, I., Halme, A., Koskinen, K. Multi-agent system enhanced supervision of process automation.
    2006 International IEEE Workshop on Distributed Intelligent Systems (DIS 2006), June 15-16, 2006, Prague, Czech Republic, pp. 151-156.
    10.1109/DIS.2006.53 - cite
  43. Seilonen, I., Pirttioja, T., Pakonen, A., Appelqvist, P., Halme, A., Koskinen, K. Information access and control operations in multi-agent system based process automation
    2nd International Conference on Industrial Applications of Holonic and Multi-Agent Systems (HoloMAS 2005), August 22-24, 2005, Copenhagen, Denmark, pp. 144-153.
    10.1007/11537847_13 - cite
  44. Pirttioja, T., Pakonen, A., Seilonen, I., Halme, A., Koskinen, K. Multi-agent based information access services for condition monitoring in process automation
    3rd IEEE International Conference on Industrial Informatics (INDIN 2005), August 10-12, 2005, Perth, Australia, pp. 240-245.
    10.1109/INDIN.2005.1560383 - cite

Theses

  1. Pakonen, A., Practical solutions for the model-checking of fault-tolerant instrumentation and control system logics.
    Doctoral Thesis, Aalto University, 2025.
    https://urn.fi/URN:ISBN:978-952-64-2647-1
  2. Pakonen, A., Information agent technology in process automation systems.
    Master's thesis, Helsinki University of Technology, 2004.
    https://urn.fi/URN:NBN:fi:aalto-2020120451022

Other

  1. Pakonen, A., Turunen, J. Using model checking for interlocking software verification.
    SIGNAL+DRAHT, 9/2023, Eurailpress, 2023.
    cite
  2. Helminen, A., Pakonen, A. Potential applications of model checking in probabilistic risk assessments.
    VTT Research Report, VTT-R-00017-20, 2020.
    cite
  3. Pakonen, A., Verification of FPGA application design by model checking.
    9th International Workshop on the Application of Field Programmable Gate Arrays in Nuclear Power Plants, October 3-6, 2016, Lyon, France.
  4. Tommila, T., Pakonen, A. Controlled natural language requirements in the design and analysis of safety critical I&C systems.
    VTT Research Report, VTT-R-01067-14, 2014.
    cite
  5. Tommila, T., Hirvonen, J., Pakonen, A. Fuzzy ontologies for retrieval of industrial knowledge: A case study.
    VTT Working Papers 153, 2010.
    cite