Сборники трудов ИСП РАН


Контрактный метод спецификации реактивных требований

А. Наумчев (Университет Иннополис, Иннополис, Россия)
М. Маццара (Университет Иннополис, Иннополис, Россия)
Б. Мейер (Университет Иннополис, Иннополис, Россия; Миланский технический университет, Милан, Италия; Университет Тулузы, Тулуза, Франция)
Ж.-М. Брюэль (Университет Тулузы, Тулуза, Франция)
Ф. Галинье (Университет Тулузы, Тулуза, Франция)
С. Эберсоль (Университет Тулузы, Тулуза, Франция)

Аннотация

Верификация многих прикладных систем – в частности, встроенных, - включает в себя процессы, исполняющиеся во времени, для моделирования которых обычно используется временная логика, линейная (LTL) или ветвящаяся (CTL). Наиболее развитые автоматические доказатели программ, однако, основаны на невременных теориях: например, на логике Хоара. Возможно ли все же применение этой развитой технологии верификации к более сложным системам? В качестве шага на пути к положительному ответу, мы разработали схему перевода подмножества LTL спецификаций в объектно-ориентированные программы с контрактами на языке Eiffel, которые являются естественными целями для доказателя программ AutoProof. Мы применили эту схему к опубликованной временной модели широко используемого реалистичного примера, авиационной системы контроля шасси, являющейся своего рода эталонной задачей для сравнения применимости различных методов спецификации. Верификация переведенной спецификации с помощью AutoProof обнаружила ошибку в одном из временных свойств. Углубленное изучение данной ошибки привело к обнаружению ошибки в опубликованной абстрактной машине состояний (ASM), которая реализует переведенную модель; авторы публикации, в свою очередь, заявили об успешной верификации. Корректировка исходной спецификации и перевод результата в Eiffel с контрактами с последующей верификацией привели к успешному результату. Процесс перевода из LTL в Eiffel все еще находится в зачаточном состоянии и оптимизирован для используемого инструмента верификации (AutoProof), поэтому схема перевода не выглядит простой и элегантной. Даже с учетом указанных ограничений полученные результаты демонстрируют потенциал технологии автоматического доказательства традиционных программ в части ее применимости к специфичным проблемам встроенных систем.

Ключевые слова

бесшовные требования; проектирование по контракту; autoproof; эйфель; система контроля шасси

Издание

Труды Института системного программирования РАН, том 29, вып. 4, 2017, стр. 39-54.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(4)-3

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома