Труды института системного программирования РАН
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Общая информация
Последний выпуск
Архив

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Труды ИСП РАН:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Труды института системного программирования РАН, 2017, том 29, выпуск 4, страницы 39–54
DOI: https://doi.org/10.15514/ISPRAS-2017-29(4)-3
(Mi tisp234)
 

A contract-based method to specify stimulus-response requirements
[Контрактный метод спецификации реактивных требований]

A. Naumcheva, M. Mazzaraa, B. Meyerabc, J.-M. Bruelc, F. Galinierc, S. Ebersoldc

a Innopolis University
b Politecnico di Milano
c Paul Sabatier University
Список литературы:
Аннотация: Верификация многих прикладных систем — в частности, встроенных, — включает в себя процессы, исполняющиеся во времени, для моделирования которых обычно используется временная логика, линейная (LTL) или ветвящаяся (CTL). Наиболее развитые автоматические доказатели программ, однако, основаны на невременных теориях: например, на логике Хоара. Возможно ли все же применение этой развитой технологии верификации к более сложным системам? В качестве шага на пути к положительному ответу, мы разработали схему перевода подмножества LTL спецификаций в объектно-ориентированные программы с контрактами на языке Eiffel, которые являются естественными целями для доказателя программ AutoProof. Мы применили эту схему к опубликованной временной модели широко используемого реалистичного примера, авиационной системы контроля шасси, являющейся своего рода эталонной задачей для сравнения применимости различных методов спецификации. Верификация переведенной спецификации с помощью AutoProof обнаружила ошибку в одном из временных свойств. Углубленное изучение данной ошибки привело к обнаружению ошибки в опубликованной абстрактной машине состояний (ASM), которая реализует переведенную модель; авторы публикации, в свою очередь, заявили об успешной верификации. Корректировка исходной спецификации и перевод результата в Eiffel с контрактами с последующей верификацией привели к успешному результату. Процесс перевода из LTL в Eiffel все еще находится в зачаточном состоянии и оптимизирован для используемого инструмента верификации (AutoProof), поэтому схема перевода не выглядит простой и элегантной. Даже с учетом указанных ограничений полученные результаты демонстрируют потенциал технологии автоматического доказательства традиционных программ в части ее применимости к специфичным проблемам встроенных систем.
Ключевые слова: бесшовные требования, проектирование по контракту, autoproof, эйфель, система контроля шасси.
Реферативные базы данных:
Тип публикации: Статья
Язык публикации: английский
Образец цитирования: A. Naumchev, M. Mazzara, B. Meyer, J.-M. Bruel, F. Galinier, S. Ebersold, “A contract-based method to specify stimulus-response requirements”, Труды ИСП РАН, 29:4 (2017), 39–54
Цитирование в формате AMSBIB
\RBibitem{NauMazMey17}
\by A.~Naumchev, M.~Mazzara, B.~Meyer, J.-M.~Bruel, F.~Galinier, S.~Ebersold
\paper A contract-based method to specify stimulus-response requirements
\jour Труды ИСП РАН
\yr 2017
\vol 29
\issue 4
\pages 39--54
\mathnet{http://mi.mathnet.ru/tisp234}
\crossref{https://doi.org/10.15514/ISPRAS-2017-29(4)-3}
\elib{https://elibrary.ru/item.asp?id=29968642}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/tisp234
  • https://www.mathnet.ru/rus/tisp/v29/i4/p39
  • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Труды института системного программирования РАН
     
      Обратная связь:
     Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024