Y. Belev, Ts. Ivanova, I. Bachkova. Cybersecurity Formal Verification of OPC-UA Applications

Кеу Words: Cybersecurity; OPC-UA applications; security; formal verification; information modeling; timed automata models; temporal logic.

Abstract. Cybersecurity protect the confidentiality, integrity and availability of computing devices and networks, hardware and software, and most importantly, data and information. The main aim of the paper is to analyze the capabilities and to propose an approach for increasing the security of OPC-UA applications based on the use of formal verification, and its integration into the development lifecycle model and information modeling capabilities provided by OPC-UA. The formal verification is based on using model checking based on timed automata models of the system and cybersecurity properties, defined by using temporal logic.