|
Эта публикация цитируется в 4 научных статьях (всего в 4 статьях)
Математические основы компьютерной безопасности
Приёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB
П. Н. Девянин, М. А. Леонова ООО «РусБИТех-Астра», г. Москва, Россия
Аннотация:
Рассматриваются приёмы по доработке описания модели управления доступом отечественной защищённой операционной системы специального назначения Astra Linux Special Edition (МРОСЛ ДП-модели) в формализованной нотации (на формализованном языке метода Event-B), основанные на использовании нескольких глобальных типов, разделении общих тотальных функций на частные тотальные функции и сокращении числа инвариантов и охранных условий событий, предполагающих перебор подмножеств некоторого множества. Результатом их применения стало упрощение автоматизированной дедуктивной верификации модели с применением инструмента Rodin и её адаптация к верификации с использованием инструмента проверки моделей ProB. Данные приёмы могут быть полезны при разработке других моделей управления доступом и их верификации с применением соответствующих инструментов.
Ключевые слова:
модель управления доступом, дедуктивная верификация, Event-B, Rodin, метод проверки моделей, ProB.
Образец цитирования:
П. Н. Девянин, М. А. Леонова, “Приёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB”, ПДМ, 2021, № 52, 83–96
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/pdm739 https://www.mathnet.ru/rus/pdm/y2021/i2/p83
|
Статистика просмотров: |
Страница аннотации: | 345 | PDF полного текста: | 141 | Список литературы: | 14 |
|