The techniques of formalization of OS Astra linux special edition access control model using Event-B formal method for verification using Rodin and ProB

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