Zobrazeno 1 - 10
of 40
pro vyhledávání: '"Antti Pakonen"'
Autor:
Polina Ovsiannikova, Antti Pakonen, Dmitry Muromsky, Maksim Kobzev, Viktor Dubinin, Valeriy Vyatkin
Publikováno v:
IEEE Open Journal of the Industrial Electronics Society, Vol 5, Pp 616-631 (2024)
The design of safety-critical cyber–physical systems requires a rigorous check of their operation logic, as well as an analysis of their overall instrumentation and control (I&C) architectures. In this article, we focus on the latter and use formal
Externí odkaz:
https://doaj.org/article/e68d9eaddc47479392ed391638d38f68
Publikováno v:
IEEE Access, Vol 9, Pp 61383-61397 (2021)
Thorough verification is a part of the design process of instrumentation and control systems if they must comply with crucial safety requirements. Model checking can be applied to the formal model of such a system to reason about its correctness base
Externí odkaz:
https://doaj.org/article/304899e3ac174de9873d6d6f2ebfcc44
Autor:
Igor Buzhinsky, Antti Pakonen
Publikováno v:
IEEE Access, Vol 8, Pp 197684-197694 (2020)
One of the approaches to assure reliability of nuclear instrumentation and control (I&C) systems is model checking, a formal verification technique. Model checking is computationally demanding, but nuclear I&C systems have certain properties that sim
Externí odkaz:
https://doaj.org/article/c4b8c5931b0a4a6d85ddfe7a546cd896
Autor:
Igor Buzhinsky, Antti Pakonen
Publikováno v:
IEEE Access, Vol 7, Pp 162139-162156 (2019)
Model checking has been successfully used for detailed formal verification of instrumentation and control (I&C) systems, as long as the focus has been on the application logic alone. In safety-critical applications, fault tolerance is also an importa
Externí odkaz:
https://doaj.org/article/c79bec426d084eee8f3fe3c47c1ae3ac
Autor:
Teemu Mätäsniemi, Antti Pakonen
Publikováno v:
IECON
Pakonen, A & Mätäsniemi, T 2021, Ontology-based approach for analyzing nuclear overall I &C architectures . in IECON 2021 – 47th Annual Conference of the IEEE Industrial Electronics Society ., 9589078, IEEE Institute of Electrical and Electronic Engineers, pp. 1-7, 47th Annual Conference of the IEEE Industrial Electronics Society, IECON 2021, Toronto, Ontario, Canada, 13/10/21 . https://doi.org/10.1109/IECON48115.2021.9589078
Pakonen, A & Mätäsniemi, T 2021, Ontology-based approach for analyzing nuclear overall I &C architectures . in IECON 2021 – 47th Annual Conference of the IEEE Industrial Electronics Society ., 9589078, IEEE Institute of Electrical and Electronic Engineers, pp. 1-7, 47th Annual Conference of the IEEE Industrial Electronics Society, IECON 2021, Toronto, Ontario, Canada, 13/10/21 . https://doi.org/10.1109/IECON48115.2021.9589078
Nuclear power plants have many different instrumentation and control (I&C) systems. Together, these systems (and their various dependencies) form the overall I&C architecture, which needs to fulfill the principle of defence-in-depth. The safety syste
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f15116aa135fafcd2e0f1dbdb55feac2
https://doi.org/10.1109/IECON48115.2021.9589078
https://doi.org/10.1109/IECON48115.2021.9589078
Publikováno v:
IECON
Ovsiannikova, P, Pakonen, A & Vyatkin, V 2021, Change-based causes in counterexample explanation for model checking . in IECON 2021 – 47th Annual Conference of the IEEE Industrial Electronics Society ., 9589122, IEEE Institute of Electrical and Electronic Engineers, pp. 1-6, 47th Annual Conference of the IEEE Industrial Electronics Society, IECON 2021, Toronto, Ontario, Canada, 13/10/21 . https://doi.org/10.1109/IECON48115.2021.9589122
Ovsiannikova, P, Pakonen, A & Vyatkin, V 2021, Change-based causes in counterexample explanation for model checking . in IECON 2021 – 47th Annual Conference of the IEEE Industrial Electronics Society ., 9589122, IEEE Institute of Electrical and Electronic Engineers, pp. 1-6, 47th Annual Conference of the IEEE Industrial Electronics Society, IECON 2021, Toronto, Ontario, Canada, 13/10/21 . https://doi.org/10.1109/IECON48115.2021.9589122
Formal verification by means of model checking avails in discovering design issues of safety systems at the early stages. However, a significant amount of time and effort is required to decipher its results and localize the failure, especially in com
Autor:
Antti Pakonen
Publikováno v:
Pakonen, A 2021, Model-checking infinite-state nuclear safety I &C systems with nuXmv . in Proceedings-2021 IEEE 19th International Conference on Industrial Informatics, INDIN 2021 ., 9557445, IEEE Institute of Electrical and Electronic Engineers, 2021 IEEE 19th International Conference on Industrial Informatics, INDIN 2021, 21/07/21 . https://doi.org/10.1109/INDIN45523.2021.9557445
INDIN
INDIN
For over a decade, model checking has been successfully used to formally verify the instrumentation and control (I&C) logic design in Finnish nuclear power plant projects. One of the practical challenges is that the model checker NuSMV forces the use
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0d50310c6cb019b7958f56448abd08ce
https://cris.vtt.fi/ws/files/53289058/Pakonen_INDIN_2021_preprint.pdf
https://cris.vtt.fi/ws/files/53289058/Pakonen_INDIN_2021_preprint.pdf
Autor:
Antti Pakonen
Publikováno v:
Pakonen, A 2021, Model-checking I &C logics — insights from over a decade of projects in Finland . in 12th Nuclear Plant Instrumentation, Control and Human-Machine Interface Technologies (NPIC &HMIT 2021) . American Nuclear Society (ANS), pp. 792-801, 12th Nuclear Plant Instrumentation, Control and Human-Machine Interface Technologies, NPIC &HMIT 2021, 14/06/21 . https://doi.org/10.13182/T124-34322
Model checking is a formal, computer-assisted verification method, used to prove that a model of a (hardware or software) system fulfills stated properties. In Finland, VTT has successfully applied the method in practical nuclear projects since 2008,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::36f5ac34f71c4fd97eca980eeec9be4a
https://cris.vtt.fi/ws/files/54526432/Pakonen_NPIC_HMIT_2021.pdf
https://cris.vtt.fi/ws/files/54526432/Pakonen_NPIC_HMIT_2021.pdf
Publikováno v:
Ovsiannikova, P, Buzhinsky, I, Pakonen, A & Vyatkin, V 2021, ' OERITTE : user-friendly counterexample explanation for model checking ', IEEE Access, vol. 9, 9405616, pp. 61383-61397 . https://doi.org/10.1109/ACCESS.2021.3073459
IEEE Access, Vol 9, Pp 61383-61397 (2021)
IEEE Access, Vol 9, Pp 61383-61397 (2021)
Thorough verification is a part of the design process of instrumentation and control systems if they must comply with crucial safety requirements. Model checking can be applied to the formal model of such a system to reason about its correctness base
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5a14f0440c801a49b7b330a31d0224ec
https://cris.vtt.fi/en/publications/06545af2-822f-4965-9ca4-a96eacc93c80
https://cris.vtt.fi/en/publications/06545af2-822f-4965-9ca4-a96eacc93c80
Publikováno v:
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 . IEEE Institute of Electrical and Electronic Engineers, pp. 697-704, 46th Annual Conference of the IEEE Industrial Electronics Society, IECON 2020, Singapore, Singapore, 18/10/20 . https://doi.org/10.1109/iecon43393.2020.9255176
IECON
IECON
Model checking methods have been proven to be a valuable asset for identifying undesired behaviour of safety-critical Instrumentation and Control (I&C) logics. Their application in the nuclear domain has been very successful and has triggered signifi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::96f6243e120d1e491f4590b956082b44
https://cris.vtt.fi/ws/files/42478670/Pakonen_et_al_IECON2020_preprint.pdf
https://cris.vtt.fi/ws/files/42478670/Pakonen_et_al_IECON2020_preprint.pdf