Применение формальных методов при проектировании коллаборационной системы противовирусной защиты

Предлагается подход, позволяющий исследовать математическую модель системы защиты от вирусов на этапе ее проектирования с помощью статистического анализа исполняемой спецификации модели, основанной на формализме распределенных объектно ориентированных стохастических гибридных систем (РООСГС). Важными аспектами модели являются ее распределенный и вероятностный характер. Эти аспекты делают модель более сложной для проведения атак, но в то же время значительно усложняют понимание ее свойств разработчиком. На данном примере мы показываем, как с помощью использования спецификации системы в качестве модели РООСГС вкупе со статистическим анализом можно исследовать ее свойства на раннем этапе проектирования и как с применением данного подхода можно обнаружить «дефекты» модели и исправить их еще в процессе ее создания.