Приемы дедуктивной верификации программного кода с использованием AstraVer Toolset

Описывается ряд практических приёмов дедуктивной верификации программного кода на языке Си на соответствие спецификациям его функций, заданных на языке ACSL. Для такой верификации используется основанный на платформе Frama-C набор инструментов AstraVer Toolset. Апробация этих приёмов осуществлена при верификации программного кода модуля управления доступом, реализованного в подсистеме безопасности PARSEC отечественной защищённой операционной системы специального назначения Astra Linux Special Edition. Благодаря использованию этих приёмов удалось упростить спецификации функций PARSEC, уменьшить трудоёмкость и ускорить процесс их дедуктивной верификации.