С каждым годом тема формальной верификации все прочнее укрепляется в разных областях технологического бизнеса России. Формальная верификация - инструмент, позволяющий доказать соответствие предмета верификации его формальному описанию.
В докладе поговорим о плюсах и минусах формальной верификации, о том, как ее применяют при разработке ПО в области информационной безопасности. Обсудим задачу создания и доказательства формальной математической модели для прохождения сертификации во ФСТЭК.
В заключение рассмотрим более общие задачи, которые можно решать с помощью формальной верификации, а также сравним такие существующие инструменты, как Event-B, CPN Tools, TLA+, COQ.