|
ИСТИНА |
Войти в систему Регистрация |
ФНКЦ РР |
||
О представлении МРОСЛ ДП-модели в формализованной нотации Event-Bстатья
- Авторы: Девянин П.Н., Кулямин В.В., Хорошилов А.В., Щепетков И.В.
- Журнал: Проблемы информационной безопасности. Компьютерные системы
- Номер: 3
- Год издания: 2014
- Первая страница: 7
- Последняя страница: 15
- Аннотация: Рассматривается подход к переходу от математической нотации представления мандатной сущностно-ролевой ДП-модели (МРОСЛ ДП-модели), ориентированной на реализацию в отечественной защищенной операционной системе специального назначения Astra Linux Special Edition (ОССН), к формализованной нотации Event-B. Такой переход позволит верифицировать описание модели и осуществить дедуктивные доказательства ее свойств, а в дальнейшем, задав на основе формализованной нотации спецификации (предусловия и постусловия) функций механизма управления доступом ОССН с использованием инструмента дедуктивной верификации кода Why, обосновать адекватность реализации модели в программном коде ОССН.
- Добавил в систему: Кулямин Виктор Вячеславович