О приемах по доработке согласованного описания МРОСЛ ДП-модели для ОС и СУБД с целью его верификации инструментами Rodin и ProB

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