Ежеквартальный журнал издательства СПбПУ
под редакцией проф. П. Д. Зегжды
Санкт-Петербургский политехнический университет Петра Великого
Институт компьютерных наук и технологий.
Кафедра информационной безопасности компьютерных систем
Проблемы информационной безопасности. Компьютерные системы
Издается с 1999 года.
ISSN 2071-8217
О представлении МРОСЛ ДП-модели в формализованной нотации Event-B

Девянин П. Н.

г. Москва, Учебно-методическое объединение вузов России по образованию в области информационной безопасности

 

Кулямин В. В., Петренко А. К., Хорошилов А. В., Щепетков И. В.

г. Москва, Институт системного программирования Российской академии наук

Аннотация:

Рассматривается подход к переходу от математической нотации представления мандатной сущностно-ролевой ДП-модели (МРОСЛ ДП-модели), ориентированной на реализацию в отечественной защищенной операционной системе специального назначения Astra Linux Special Edition (ОССН), к формализованной нотации Event-B. Такой переход позволит верифицировать описание модели и осуществить дедуктивные доказательства ее свойств, а в дальнейшем, задав на основе формализованной нотации спецификации (предусловия и постусловия) функций механизма управления доступом ОССН с использованием инструмента дедуктивной верификации кода Why, обосновать адекватность реализации модели в программном коде ОССН.

Ключевые слова: Компьютерная безопасность, ДП-модель, Event-B, операционная система Astra Linux.
Страницы 7-15