Application of formal methods in the design of a collaborative virus defense system

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.