Formal Verification of STPA with Model Checking
As technology advances, hardware-centric systems are rapidly moving towards software-centric ones, and their complexity is rapidly increasing. In particular, systems directly related to safety require thorough verification. Model checking exhaustively explores the state space of the abstracted syst...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Gdynia Maritime University
2023-03-01
|
| Series: | Scientific Journal of Gdynia Maritime University |
| Subjects: | |
| Online Access: | https://ojs.umg.edu.pl/index.php/sjgmu/article/view/299 |
| _version_ | 1797197194582818816 |
|---|---|
| author | Ryeonggu Kwon Gihwon Kwon |
| author_facet | Ryeonggu Kwon Gihwon Kwon |
| author_sort | Ryeonggu Kwon |
| collection | DOAJ |
| description |
As technology advances, hardware-centric systems are rapidly moving towards software-centric ones, and their complexity is rapidly increasing. In particular, systems directly related to safety require thorough verification. Model checking exhaustively explores the state space of the abstracted system to check whether properties written in a logical formula are achieved. In this paper, the control algorithm of the controller is verified using model checking to discover risk scenarios during the STPA steps. Two case studies are conducted using the widely used model checkers NuSMV and UPPAAL. We then explain the empirical results and compare two model checkers based on their characteristics. Finally, we discuss the benefits of applying model checking in the process of STPA.
|
| first_indexed | 2024-04-24T06:40:05Z |
| format | Article |
| id | doaj.art-981bb5175b4e49c0940ac251872c00d6 |
| institution | Directory Open Access Journal |
| issn | 2657-5841 2657-6988 |
| language | English |
| last_indexed | 2024-04-24T06:40:05Z |
| publishDate | 2023-03-01 |
| publisher | Gdynia Maritime University |
| record_format | Article |
| series | Scientific Journal of Gdynia Maritime University |
| spelling | doaj.art-981bb5175b4e49c0940ac251872c00d62024-04-23T03:13:36ZengGdynia Maritime UniversityScientific Journal of Gdynia Maritime University2657-58412657-69882023-03-0112510.26408/125.01Formal Verification of STPA with Model CheckingRyeonggu Kwon0Gihwon Kwon Kyonggi University, 6, Seowon 4-gil, Gwanak-gu, Seoul, Republic of Korea, Department of Computer Science As technology advances, hardware-centric systems are rapidly moving towards software-centric ones, and their complexity is rapidly increasing. In particular, systems directly related to safety require thorough verification. Model checking exhaustively explores the state space of the abstracted system to check whether properties written in a logical formula are achieved. In this paper, the control algorithm of the controller is verified using model checking to discover risk scenarios during the STPA steps. Two case studies are conducted using the widely used model checkers NuSMV and UPPAAL. We then explain the empirical results and compare two model checkers based on their characteristics. Finally, we discuss the benefits of applying model checking in the process of STPA. https://ojs.umg.edu.pl/index.php/sjgmu/article/view/299formal verification, model checking, STPA |
| spellingShingle | Ryeonggu Kwon Gihwon Kwon Formal Verification of STPA with Model Checking Scientific Journal of Gdynia Maritime University formal verification, model checking, STPA |
| title | Formal Verification of STPA with Model Checking |
| title_full | Formal Verification of STPA with Model Checking |
| title_fullStr | Formal Verification of STPA with Model Checking |
| title_full_unstemmed | Formal Verification of STPA with Model Checking |
| title_short | Formal Verification of STPA with Model Checking |
| title_sort | formal verification of stpa with model checking |
| topic | formal verification, model checking, STPA |
| url | https://ojs.umg.edu.pl/index.php/sjgmu/article/view/299 |
| work_keys_str_mv | AT ryeonggukwon formalverificationofstpawithmodelchecking AT gihwonkwon formalverificationofstpawithmodelchecking |