ГОСТ Р 59453.2-2021 Защита информации. Формальная модель управления доступом. Часть 2. Рекомендации по верификации формальной модели управления доступом

     7 Верификация формализованного (машиночитаемого) описания формальной модели управления доступом

7.1 При верификации формальной модели управления доступом выбранные в соответствии с 5.3 инструментальные средства верификации должны быть применены к ее формализованному (машиночитаемому) описанию, полученному в соответствии с 6.1.

7.2 Верификация формализованного (машиночитаемого) описания формальной модели управления доступом с применением инструментальных средств должна состоять в выполнении следующих действий:

- должно быть осуществлено автоматическое доказательство непротиворечивости формальной модели и выполнения заданных в ее рамках условий безопасности (условий верификации) при наличии у инструментальных средств соответствующей функциональности, в противном случае должно быть выполнено интерактивное доказательство этих условий верификации;