Каннер, Андрей Михайлович.
    Применение TLA+ нотации для описания модели изолированной программной среды субъектов доступа и ее дальнейшей верификации [Текст] / А. М. Каннер // Вопросы защиты информации. - 2021. - № 3. - С. 8-11 . - ISSN 2073-2600
УДК
ББК 32.97
Рубрики: Вычислительная техника
   Вычислительная техника в целом

Кл.слова (ненормированные):
Лампорта действия -- верификация модели -- действия Лампорта -- математические обозначения -- метод проверки модели -- модели безопасности -- модель IPES -- спецификация модели
Аннотация: Рассматриваются недостатки проверки математических обозначений моделей безопасности, в частности модель изолированной программной среды субъектов, ее спецификация дана в нотации TLA+ и описаны преимущества проверки этой спецификации с помощью специализированных инструментов.

Нет сведений об экземплярах (Источник в БД не найден)