Сравнение способов моделирования механизмов управления доступом ОС и СУБД на формализованном языке метода Event-B с целью их верификации инструментами Rodin и ProB

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