Formal verification of STPA with model checking

• Autorzy: Kwon Ryeonggu , Kwon Gihwon

Identyfikatory

DOI

10.26408/125.01

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

formal verification; model checking; STPA

• Wydawca: Publishing House of Gdynia Maritime University
• Czasopismo: Scientific Journal of Gdynia Maritime University
• Rocznik: 2023
• Tom: nr 125
• Strony: 7--24
• Opis fizyczny: Bibliogr. 10 poz., tab.

Twórcy

autor

Kwon Ryeonggu

• Kyonggi University, 6, Seowon 4-gil, Gwanak-gu, Seoul, Republic of Korea, Department of Computer Science

• https://orcid.org/0000-0002-4942-247X

autor

Kwon Gihwon

• Kyonggi University, 6, Seowon 4-gil, Gwanak-gu, Seoul, Republic of Korea, Department of Computer Science

• https://orcid.org/0000-0002-8221-4939

Bibliografia

• 1. Abdulkhaleq, A., Wagner, S., Leveson, N., 2015, A Comprehensive Safety Engineering Approach for Software-Intensive Systems Based on STPA, Procedia Engineering, vol. 128, pp. 2–11.
• 2. Baier, C., Katoen, J.-P., Larsen, K.G., 2014, Principles of Model Checking, MIT Press, Cambridge.
• 3. Dakwat, A.L., Villani, E., 2018, System Safety Assessment Based on STPA and Model Checking, Safety Science, vol. 109, pp. 130–143.
• 4. De Souza, F.G., de Melo Bezerra, J., Hirata, C.M., de Saqui-Sannes, P., Apvrille, L., 2020, Combining STPA with SysML Modeling, 2020 IEEE International Systems Conference (SysCon).
• 5. Placke, M.S., 2014a, Application of STPA to the Integration of Multiple Control Systems: A Case Study and New Approach.
• 6. Tsuji, M., Takai, T., Kakimoto, K., Ishihama, N., Katahira, M., Iida, H., 2020, Prioritizing Scenarios Based on Stamp/STPA Using Statistical Model Checking, 2020 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW).
• 7. Zhong, D., Sun, R., Gong, H., Wang, T., 2022, System-Theoretic Process Analysis Based on SysML/Marte and NuSMV, Applied Sciences, vol. 12(3).
• 8. Leveson, N.G., Thomas, J.P., 2018, STPA Handbook, http://psas.scripts.mit.edu/home/¬get_file.php?-name=STPA_handbook.pdf (accessed 23.08.2022).
• 9. Placke, M.S., 2014b, Engineering a Safer World, http://sunnyday.mit.edu/safer-world.pdf (accessed 23.08.2022).

Uwagi

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023).