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