
Application of formal methods in the design of a collaborative virus defense system
Author(s) -
Роман Евгеньевич Шарыкин,
Александр Николаевич Курбацкий
Publication year - 2020
Publication title -
žurnal belorusskogo gosudarstvennogo universiteta. matematika, informatika/žurnal belorusskogo gosudarstvennogo universiteta. matematika, informatika
Language(s) - English
Resource type - Journals
eISSN - 2617-3956
pISSN - 2520-6508
DOI - 10.33581/2520-6508-2020-1-59-69
Subject(s) - executable , computer science , formalism (music) , formal methods , probabilistic logic , formal specification , statistical model , software engineering , theoretical computer science , distributed computing , formal verification , programming language , artificial intelligence , art , musical , visual arts
This article proposes an approach that allows us to study a mathematical model of a virus protection system at the stage of its design using statistical analysis of an executable model specification based on the formalism of Distributed Object Based Stochastic Hybrid Systems (DOBSHS). Important aspects of the model are its distributed and probabilistic nature. These aspects make the model more difficult to carry out attacks, but at the same time significantly complicate the understanding of its properties by the developer. In this example, we show how, using the specification of the system as a DOBSHS model, coupled with its statistical analysis, we can investigate its properties at an early stage of design and how, using this approach, we can detect «defects» of the model and correct them during the process of creating the model.