Войти / Регистрация
Корзина

  • Ваша корзина пуста
Войти / Регистрация
Корзина

  • Ваша корзина пуста

Статья «Сравнение способов декомпозиции спецификаций на Event-B, "Программирование"»

Авторы:
  • Девянин П.Н.1
  • Кулямин В.В.2
  • Петренко А.К.3
  • Хорошилов А.В.4
  • Щепетков И.В.5
стр. 17-26
Платно
1 Учебно-методическое объединение по образованию в области информационной безопасности, 2 Институт системного программирования РАН; Московский государственный университет им. М.В. Ломоносова; НИУ "Высшая школа экономики", 3 Институт системного программирования РАН; Московский государственный университет им. М.В. Ломоносова; НИУ "Высшая школа экономики", 4 Институт системного программирования РАН; Московский физико-технический институт (государственный университет), 5 Институт системного программирования РАН
  • В выпуске: №4, 2016
  • В журнале: Программирование
  • Издательство: ФГУП «Издательство «Наука»
  • Рубрика ГРНТИ: Информатика. Информационные и вычислительные системы
  • Год выхода: 2016
  • SDI: 007.001.0132-3474.2016.000.004.17.26
  • ISSN: 0132-3474
Аннотация:
Декомпозиция является важным шагом при построении систем среднего и крупного размера. Исследованию различных архитектур программных систем и методов декомпозиции, в частности, посвящено множество работ. На текущий момент формальные спецификации программных систем используются в основном только в экспериментальных целях, и по этой причине их размер и сложность относительно невелики. Как следствие, при разработке нетривиальной спецификации возникает вопрос сравнения между собой возможных подходов к декомпозиции для выбора наиболее подходящего. В статье анализируется опыт, полученный при дедуктивной верификации формальной спецификации мандатной сущностно-ролевой модели управления доступом и информационными потоками в ОС семейства Linux (МРОСЛ ДП-модель) с использованием формального метода Event" В и техники пошагового уточнения. В ней сопоставляются два подхода к декомпозиции спецификации с помощью уточнения, а также исследуются источники и характеристики сложности архитектуры модели.

Архивные статьи (2015 год и ранее) доступны для ознакомления бесплатно, для скачивания их необходимо приобрести. Для просмотра материалов необходимо зарегистрироваться и авторизоваться на сайте.

Чтобы приобрести доступ к материалу для юридического лица, пожалуйста, свяжитесь с администрацией портала с помощью формы обратной связи либо по электронному адресу libnauka@naukaran.com.  

Действия с материалами доступны только авторизованным пользователям.