Главная Упрощенный режим Описание Шлюз Z39.50
Авторизация
Фамилия
Пароль
 

Базы данных


- результаты поиска

Вид поиска
Книги фонда НБ СГЮА
Дипломные работы выпускников СГЮА за последние 5 лет
Авторефераты
Диссертации
Период.издания науч.абонемента
Редкие книги Научной библиотеки СГЮА
Каталог электронных носителей
Труды ученых СГЮА
Саратовский край
Область поиска
Формат представления найденных документов:
полныйинформационныйкраткий
Поисковый запрос: (<.>K=действия Лампорта<.>)
Общее количество найденных документов : 1
1.


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

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

Найти похожие
 
Стандартный
Расширенный
Профессиональный
Распределенный
По словарю
ГРНТИ-навигатор
УДК-навигатор
ББК-навигатор
Тематический навигатор
© Международная Ассоциация пользователей и разработчиков электронных библиотек и новых информационных технологий
(Ассоциация ЭБНИТ)