@article{PakonenJSS2024,
title = {Evaluation of visual property specification languages based on practical model-checking experience},
journal = {Journal of Systems and Software},
volume = {216},
pages = {112153},
year = {2024},
doi = {10.1016/j.jss.2024.112153},
url = {},
author = {Antti Pakonen and Igor Buzhinsky and Valeriy Vyatkin}
}
@article{OvsiannikovaOJIES2024,
title = {Formal verification of non-functional requirements of overall instrumentation and control architectures},
journal = {IEEE Open Journal of the Industrial Electronics Society},
author = {Polina Ovsiannikova and Anti Pakone and Dmitry Muromsky and Maksim Kobzev and Viktor Dubinin and Valeriy Vyatkin},
year={2024},
volume={5},
number={},
pages={616-631},
doi={10.1109/OJIES.2024.3413568}
}
@article{OvsiannikovaACCESS2021,
author={Ovsiannikova, Polina and Buzhinsky, Igor and Pakonen, Antti and Vyatkin, Valeriy},
journal={IEEE Access},
title={Oeritte: User-Friendly Counterexample Explanation for Model Checking},
year={2021},
volume={9},
number={},
pages={61383-61397},
doi={10.1109/ACCESS.2021.3073459}
}
@article{PakonenRESS2021,
title = {Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems},
journal = {Reliability Engineering \& System Safety},
volume = {205},
pages = {107237},
year = {2021},
issn = {0951-8320},
doi = {https://doi.org/10.1016/j.ress.2020.107237},
url = {https://www.sciencedirect.com/science/article/pii/S0951832020307377},
author = {Antti Pakonen and Igor Buzhinsky and Kim Bj\"{o}rkman}
}
@article{BuzhinskyAccess2020,
author = {I. {Buzhinsky} and A. {Pakonen}},
journal = {IEEE Access},
title = {Symmetry Breaking in Model Checking of Fault-Tolerant Nuclear Instrumentation and Control Systems},
year = {2020},
volume = {8},
number = {},
pages = {197684-197694},
doi= {10.1109/ACCESS.2020.3034799}
}
@article{BuzhinskyAccess2019,
author = {I. {Buzhinsky} and A. {Pakonen}},
journal = {IEEE Access},
title = {Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions},
year = {2019},
volume = {7},
number = {},
pages = {162139-162156},
doi = {10.1109/ACCESS.2019.2951938}
}
@InProceedings{PakonenNPIC2025,
author = {A. {Pakonen} and L. {Tuominen} and M. {Viitasalo} and P. {Nuutinen}},
booktitle = {14th Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies (NPIC \& HMIT)},
title = {Formal Safety Assessment Methods in {Olkiluoto} 1\&2 {NPP} {I\&C} Renewal Project {DIMA}},
year = {2025},
volume = {},
number = {},
pages = {},
doi = {10.13182/NPICHMIT25-46672},
url = {}
}
@InProceedings{PakonenNPIC2025,
author = {J. {Berger} and A. {King} and A. {Pakonen}},
booktitle = {14th Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies (NPIC \& HMIT)},
title = {Integrating {STPA} to {NPP} Systems Engineering Processes},
year = {2025},
volume = {},
number = {},
pages = {},
doi = {10.13182/NPICHMIT25-46634},
url = {}
}
@InProceedings{PakonenETFA2024,
author = {A. {Pakonen}},
booktitle = {29th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2024)},
title = {Compositional verification of nuclear safety {I\&C} systems with {OCRA}},
year = {2024},
volume = {},
number = {},
pages = {},
doi = {10.1109/ETFA61755.2024.10711009},
url = {}
}
@InProceedings{BergerETFA2024,
author = {J. {Berger} and R. {Tiusanen} and H. {Kothalawala} and A. {Pakonen}},
booktitle = {29th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2024)},
title = {Applying priority-informed {STPA} to a nuclear {I\&C} system},
year = {2024},
volume = {},
number = {},
pages = {},
doi = {10.1109/ETFA61755.2024.10710653},
url = {}
}
@InProceedings{OvsiannikovaIECON2023,
author = {P. {Ovsiannikova} and A. {Pakonen} and V. {Vyatkin}},
booktitle = {49th Annual Conference of the IEEE Industrial Electronics Society (IECON 2023)},
title = {Automatic generation of repair suggestions for control logic of I\&C systems},
year = {2023},
volume = {},
number = {},
pages = {},
doi = {10.1109/IECON51785.2023.10311970},
url = {},
note = {}
}
@InProceedings{PakonenETFA2023,
author = {A. {Pakonen}},
booktitle = {28th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2023)},
title = {Obfuscation of function block diagrams},
year = {2023},
volume = {},
number = {},
pages = {},
doi = {10.1109/ETFA54631.2023.10275363},
url = {}
}
@InProceedings{OvsiannikovaETFA2023,
author = {P. {Ovsiannikova} and A. {Pakonen} and V. {Vyatkin}},
booktitle = {28th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2023)},
title = {Automatic generation of repair suggestions for overall I\&C architecture represented with an ontology},
year = {2023},
volume = {},
number = {},
pages = {},
doi = {},
url = {10.1109/ETFA54631.2023.10275557}
}
@InProceedings{PakonenNPIC2023,
author = {A. {Pakonen}},
booktitle = {13th Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies (NPIC \& HMIT)},
title = {Model-checking {I\&C} logics \textendash practical examples},
year = {2023},
volume = {},
number = {},
pages = {1610-1619},
doi = {10.13182/NPICHMIT23-41122},
url = {}
}
@InProceedings{PakonenNPIC2023,
author = {K. {Bj\"{o}rkman}, A. {Pakonen}},
booktitle = {13th Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies (NPIC \& HMIT)},
title = {Analyzing defense-in-depth properties of nuclear power plant instrumentation and control system architectures using ontologies},
year = {2023},
volume = {},
number = {},
pages = {1590-1599},
doi = {10.13182/NPICHMIT23-41042},
url = {}
}
@InProceedings{PakonenNPIC2023,
author = {J. {Linnosmaa}, A. {Pakonen}, J. {Alanen}},
booktitle = {13th Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies (NPIC \& HMIT)},
title = {Demonstration of a model-based approach for formal verification of {I\&C} logics},
year = {2023},
volume = {},
number = {},
pages = {1441-1450},
doi = {10.13182/NPICHMIT23-41121},
url = {}
}
@InProceedings{PakonenIECON2021,
author = {A. {Pakonen} and T. {M\"{a}t\"{a}sniemi}},
booktitle = {The 47th Annual Conference of the IEEE Industrial Electronics Society (IECON 2021)},
title = {Ontology-based approach for analyzing nuclear overall {I\&C} architectures},
year={2021},
volume={},
number={},
pages={},
doi={10.1109/IECON48115.2021.9589078}
}
@InProceedings{OvsiannikovaIECON2021,
author = {P. {Ovsiannikova} and A. {Pakonen} and V. {Vyatkin}},
booktitle = {The 47th Annual Conference of the IEEE Industrial Electronics Society (IECON 2021)},
title = {Change-based causes in counterexample explanation for model checking},
year={2021},
volume={},
number={},
pages={},
doi={10.1109/IECON48115.2021.9589122}
}
@InProceedings{PakonenISOFIC2021,
author = {A. {Pakonen}},
booktitle = {International Symposium on Future I\&C for Nuclear Power Plants (ISOFIC 2021)},
title = {Oops! {Examples} of {I\&C} design issues detected with model checking},
year = {2021},
volume = {},
number = {},
pages = {},
doi = {},
url = {)
}
@InProceedings{PakonenINDIN2021,
author = {A. {Pakonen}},
booktitle = {The 19th IEEE International Conference on Industrial Informatics (INDIN 2021)},
title = {Model-checking infinite-state nuclear safety {I\&C} systems with {nuXmv}},
year = {2021},
volume = {},
number = {},
pages = {},
doi={10.1109/INDIN45523.2021.9557445}
}
@InProceedings{PakonenNPIC2021,
author = {A. {Pakonen}},
booktitle = {12th International Topical Meeting on Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies (NPIC \& HMIT)},
title = {Model-checking of {I\&C} logics \textendash insights from over a decade of projects in {Finland}},
year = {2021},
volume = {},
number = {},
pages = {792-801},
doi = {10.13182/T124-34322},
url = {}
}
@InProceedings{OvsiannikovaICECCS2020,
author = {P. {Ovsiannikova} and I. {Buzhinsky} and A. {Pakonen} and V. {Vyatkin}},
booktitle = {25th International Conference on Engineering of Complex Computer Systems (ICECCS 2020)},
title = {Visual counterexample explanation for model checking with {Oeritte}},
year={2021},
volume={},
number={},
pages={1-10},
doi={10.1109/ICECCS51672.2020.00008}
}
@InProceedings{PakonenIECON2020,
author = {A. {Pakonen} and P. {Biswas} and N. {Papakonstantinou}},
booktitle = {The 46th Annual Conference of the IEEE Industrial Electronics Society (IECON 2020)},
title = {Transformation of non-standard nuclear {I\&C} logic drawings to formal verification models},
year={2020},
volume={},
number={},
pages={697-704},
doi={10.1109/IECON43393.2020.9255176}
}
@InProceedings{LinnosmaaIECON2020,
author = {J. {Linnosmaa} and A. {Pakonen} and N. {Papakonstantinou} and P. {Karpati}},
booktitle = {The 46th Annual Conference of the IEEE Industrial Electronics Society (IECON 2020)},
title = {Applicability of {AADL} in modelling the overall {I\&C} architecture of a nuclear power plant},
year={2020},
volume={},
number={},
pages={4337-4344},
doi={10.1109/IECON43393.2020.9254226}
}
@InProceedings{BuzhinskyINDIN2020,
author = {I. {Buzhinsky} and A. {Pakonen}},
booktitle = {The 18th IEEE International Conference on Industrial Informatics (INDIN 2020)},
title = {Timed model checking of fault-tolerant nuclear {I\&C} systems},
year = {2020},
volume = {},
number = {},
pages = {159-164},
doi={10.1109/INDIN45582.2020.9442188}
}
@InProceedings{PakonenICIT2019,
author = {A. {Pakonen} and I. {Buzhinsky}},
booktitle = {The 20th IEEE International Conference on Industrial Technology (ICIT 2019)},
title = {Verification of fault tolerant safety {I\&C} systems using model checking},
year = {2019},
volume = {},
number = {},
pages = {969-974},
doi = {10.1109/ICIT.2019.8755014}
}
@InProceedings{BjorkmanESREL2019,
author = {K. {Bj\"{o}rkman} and A. {Pakonen}},
booktitle = {The 29th European Safety and Reliability Conference (ESREL 2019)},
title = {Coupling Model Checking and {PSA} \textendash A Case Study},
year = {2019},
volume = {},
number = {},
pages = {2789-2796},
doi = {10.3850/978-981-11-2724-3_0418-cd}
}
@InProceedings{PakonenINDIN2018,
author = {A. {Pakonen} and I. {Buzhinsky} and V. {Vyatkin}},
booktitle = {The 16th IEEE International Conference on Industrial Informatics (INDIN 2018)},
title = {Counterexample visualization and explanation for function block diagrams},
year = {2018},
volume = {},
number = {},
pages = {747-753},
doi = {10.1109/INDIN.2018.8472025}
}
@InProceedings{BuzhinskyISIE2018,
author = {I. {Buzhinsky} and A. {Pakonen} and V. {Vyatkin}},
booktitle = {The 27th IEEE International Symposium on Industrial Electronics (ISIE 2018)},
title = {Synthesis-Aided Reliability Assurance of Basic Block Models for Model Checking Purposes},
year = {2018},
volume = {},
number = {},
pages = {669-674},
doi = {10.1109/ISIE.2018.8433793}
}
@InProceedings{PakonenESREL2017,
author = {A. {Pakonen} and K. {Bj\"{o}rkman}},
booktitle = {The 27th European Safety and Reliability Conference (ESREL 2017)},
title = {Model checking as a protective method against spurious actuation of industrial control systems},
year = {2017},
volume = {},
number = {},
pages = {},
doi = {},
url = {https://cris.vtt.fi/files/23031295/Pakonen_ESREL2017_Accepted_Manuscript.pdf}
}
@InProceedings{PakonenNPIC2017,
author = {A. {Pakonen} and T. {Tahvonen} and M. {Hartikainen} and M. {Pihlanko}},
booktitle = {10th ANS International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC \& HMIT 2017)},
title = {Practical applications of model checking in the {Finnish} nuclear industry},
year = {2017},
volume = {},
number = {},
pages = {},
doi = {},
url = {http://www.vtt.fi/inf/julkaisut/muut/2017/OA-Practical_applications_of_model_checking.pdf}
}
@InProceedings{BuzhinskyIECON2017explicit,
author = {I. {Buzhinsky} and A. {Pakonen} and V. {Vyatkin}},
booktitle = {The 43rd Annual Conference of the IEEE Industrial Electronics Society (IECON 2017},
title = {Explicit-state and symbolic model checking of nuclear {I\&C} systems: A comparison},
year = {2017},
volume = {},
number = {},
pages = {5439-5446},
doi = {10.1109/IECON.2017.8216942}
}
@InProceedings{BuzhinskyIECON2017scalable,
author = {I. {Buzhinsky} and A. {Pakonen} and V. {Vyatkin}},
booktitle = {The 43rd Annual Conference of the IEEE Industrial Electronics Society (IECON 2017)},
title = {Scalable methods of discrete plant model generation for closed-loop model checking},
year = {2017},
volume = {},
number = {},
pages = {5483-5488},
doi = {10.1109/IECON.2017.8216949}
}
@InProceedings{PakonenETFA2016,
author = {A. {Pakonen} and C. {Pang} and I. {Buzhinsky} and V. {Vyatkin}},
booktitle = {The 21st IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2016)},
title = {User-friendly formal specification languages \textendash conclusions drawn from industrial experience on model checking},
year = {2016},
volume = {},
number = {},
pages = {},
doi = {10.1109/ETFA.2016.7733717}
}
@InProceedings{PangINDIN2016,
author = {C. {Pang} and A. {Pakonen} and I. {Buzhinsky} and V. {Vyatkin}},
booktitle = {2016 IEEE 14th International Conference on Industrial Informatics (INDIN)},
title = {A study on user-friendly formal specification languages for requirements formalization},
year = {2016},
volume ={},
number = {},
pages = {676-682},
doi = {10.1109/INDIN.2016.7819246}
}
@InProceedings{PakonenAutomaatio2015,
author = {A. {Pakonen} and J. {Valkonen} and S. {Matinaho} and M. {Hartikainen}},
booktitle = {Automaatio XXI},
title = {Model checking of I&C software in the Loviisa NPP automation renewal project},
year = {2015},
volume = {},
number = {},
pages = {676-682},
doi = {},
url = {https://www.automaatioseura.fi/site/assets/files/1550/f2045.pdf)
}
@InProceedings{PakonenISOFIC2014,
author = {A. {Pakonen} and J. {Valkonen} and S. {Matinaho} and M. {Hartikainen}},
booktitle = {International Symposium on Future I&C for Nuclear Power Plants (ISOFIC 2014)},
title = {Model checking for licensing support in the {Finnish} nuclear industry},
year = {2014},
volume = {},
number = {},
pages = {},
doi = {},
url = {http://www.vtt.fi/inf/julkaisut/muut/2014/ISOFIC_2014_Pakonen_et_al_FINAL.pdf)
}
@InProceedings{PakonenETFA2013,
author = {A. {Pakonen} and T. {M\"{a}t\"{a}sniemi} and J. {Lahtinen} and T. {Karhela}},
booktitle = {The 18th IEEE International Conference on Emerging Technologies \& Factory Automation (ETFA 2013)},
title = {A toolset for model checking of {PLC} software},
year = {2013},
volume = {},
number = {},
pages = {},
doi = {10.1109/ETFA.2013.6648065}
}
@InProceedings{TimonenKEOD2013,
author = {Mika Timonen and Antti Pakonen and Teemu Tommila},
title = {Using Associations and Fuzzy Ontologies for Modeling Chemical Safety Information},
booktitle = {The 2013 International Conference on Knowledge Engineering and Ontology Development (KEOD 2013)},
year = {2013},
pages = {26-37},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004536400260037},
isbn={978-989-8565-81-5},
}
@InProceedings{PakonenNPIC2012,
author = {A. {Pakonen} and T. {M\"{a}t\"{a}sniemi} and J. {Valkonen}},
booktitle = {The 8th ANS International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC \& HMIT 2012)},
title = {Model checking reveals hidden errors in safety-critical {I\&C} software},
year = {2012},
volume = {},
number = {},
pages = {},
doi = {}
}
@InProceedings{PakonenETFA2010,
author = {A. {Pakonen} and T. {Tommila} and J. {Hirvonen}},
booktitle = {The 15th IEEE International Conference on Emerging Technologies \& Factory Automation (ETFA 2010)},
title = {A fuzzy ontology based approach for mobilising industrial plant knowledge},
year={2010},
volume={},
number={},
pages={},
doi={10.1109/ETFA.2010.5641200}
}
@InProceedings{HirvonenKEOD2010,
author = {Juhani Hirvonen and Teemu Tommila and Antti Pakonen and Christer Carlsson and Mario Fedrizzi and Robert Full\'{e}r.},
title = {Fuzzy keyword ontology for annotating and searching event reports},
booktitle = {The 2010 International Conference on Knowledge Engineering and Ontology Development (KEOD 2010)},
year = {2010},
pages = {251-256},
publisher = {SciTePress},
organization = {INSTICC},
doi = {10.5220/0003091002510256},
isbn = {978-989-8425-29-4},
}
@InProceedings{PakonenNPIC2010,
author = {A. {Pakonen} and J. {Lahtinen} and V.-P. {Kuutti} and T. {Karhela}},
booktitle = {The 8th ANS International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC \& HMIT 2012)},
title = {Integrating model checking with safety-critical {I\&C} software design},
year = {2010},
volume = {},
number = {},
pages = {},
doi = {}
}
@InProceedings{PakonenETFA2007,
author = {A. {Pakonen} and T. {Tommila} and T. {Pirttioja} and I. {Seilonen}},
booktitle = {The 12th IEEE International Conference on Emerging Technologies and Factory Automation (EFTA 2007)},
title = {{OWL} based information agent services for process monitoring},
year={2007},
volume={},
number={},
pages={9-16},
doi={10.1109/EFTA.2007.4416747}
}
@InProceedings{PirttiojaHOLOMAS2007,
author = {Pirttioja, Teppo and Seilonen, Ilkka and Pakonen, Antti and Halme, Aarne and Koskinen, Kari},
editor = {Ma{\v{r}}{\'i}k, Vladim{\'i}r and Vyatkin, Valeriy and Colombo, Armando W.},
title = {Information Agents Handling Semantic Data as an Extension to Process Monitoring Systems},
booktitle = {Holonic and Multi-Agent Systems for Manufacturing},
year = {2007},
publisher = {Springer Berlin Heidelberg},
address= {Berlin, Heidelberg,
pages = {411-420},
doi = {10.1007/978-3-540-74481-8_39}
}
@InProceedings{PakonenETFA2006,
author = {A. {Pakonen} and T. {Pirttioja} and I. {Seilonen} and T. {Tommila}},
booktitle = {The 11th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2006)},
title = {Proactive Computing in Process Monitoring: Information Agents for Operator Support},
year={2006},
volume={},
number={},
pages={153-158},
doi={10.1109/ETFA.2006.355408}
}
@InProceedings{SeilonenINDIN2006,
author = {I. {Seilonen} and T. {Pirttioja} and A. {Halme} and K. {Koskinen} and A. {Pakonen}},
booktitle = {The 4th IEEE International Conference on Industrial Informatics (INDIN 2006)},
title = {Indirect Process Monitoring with Constraint Handling Agents},
year={2006},
volume={},
number={},
pages={1323-1328},
doi={10.1109/INDIN.2006.275851}
}
@InProceedings{PirttiojaDIS2006",
author = {T. {Pirttioja} and A. {Halme} and A. {Pakonen} and I. {Seilonen} and K. {Koskinen}},
booktitle = {2006 IEEE Workshop on Distributed Intelligent Systems: Collective Intelligence and Its Applications (DIS 2006)},
title = {Multi-Agent System Enhanced Supervision of Process Automation},
year={2006},
volume={},
number={},
pages={151-156},
doi={10.1109/DIS.2006.53}
}
@InProceedings{SeilonenHOLOMAS2005,
author = {Seilonen, Ilkka and Pirttioja, Teppo and Pakonen, Antti and Appelqvist, Pekka and Halme, Aarne and Koskinen, Kari},
editor = {Ma{\v{r}}{\'i}k, Vladim{\'i}r and William Brennan, Robert and P{\v{e}}chou{\v{c}}ek, Michal},
title = {Information Access and Control Operations in Multi-agent System Based Process Automation},
booktitle = {Holonic and Multi-Agent Systems for Manufacturing},
year = {2005},
publisher = {Springer Berlin Heidelberg},
address = {Berlin, Heidelberg},
pages = {144-153},
isbn = {978-3-540-31831-6},
doi = {10.1007/11537847_13}
}
@InProceedings{PirttiojaINDIN2005,
author = {T. {Pirttioja} and A. {Pakonen} and I. {Seilonen} and A. {Halme} and K. {Koskinen}},
booktitle = {The 3rd IEEE International Conference on Industrial Informatics (INDIN 2005)},
title = {Multi-agent based information access services for condition monitoring in process automation},
year = {2005},
volume = {},
number = {},
pages = {240-245},
doi = {10.1109/INDIN.2005.1560383}
}
@article{PakonenSD2023,
author={Pakonen, Antti and Turunen, Juha},
journal={SIGNAL+DRAHT},
title={Using model checking for interlocking software verification},
year={2023},
volume={},
number={9},
pages={},
doi={}
}
@techreport{HelminenVTT2020,
author = {A. Helminen and A. Pakonen},
type = {VTT Technical Report},
number = {VTT-R-00017-20},
year = {2020},
title = {Potential applications of model checking in probabilistic risk assessments},
url = {https://cris.vtt.fi/files/27299692/VTT_R_00017_20.pdf},
institution = {VTT Technical Research Centre of Finland Ltd.}
}
@techreport{TommilaVTT2014,
author = {T. Tommila and A. Pakonen},
type = {VTT Research Report},
number = {VTT-R-01067-14},
year = {2014},
title = {Controlled natural language requirements in the design and analysis of safety critical {I\&C} systems},
url = {https://www.vttresearch.com/sites/default/files/julkaisut/muut/2014/VTT-R-01067-14.pdf},
institution = {VTT Technical Research Centre of Finland Ltd.}
}
@techreport{TommilaVTT2010,
author = {T. Tommila and J. Hirvonen and A. Pakonen},
type = {VTT Working Papers},
number = {153},
year = {2010},
title = {Fuzzy ontologies for retrieval of industrial knowledge: A case study},
url = {http://www.vtt.fi/inf/pdf/workingpapers/2010/W153.pdf},
institution = {VTT Technical Research Centre of Finland Ltd.}
}