Формальная верификация при разработке ПО

Безопасность

Доклад отклонён

Тезисы

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

Системный аналитик

ИнфоТекс

Компания «ИнфоТеКС» (АО «Информационные Технологии и Коммуникационные Системы») — ведущий отечественный разработчик и производитель высокотехнологичных программных и программно-аппаратных средств защиты информации.

Видео