Введение 4
1. Цель и постановка задачи 7
2. Обзор 8
2.1. Выбор метода верификации 8
2.2. Требования к инструменту верификации 9
2.3. Выбор верификатора 10
2.4. Инструменты автоматической генерации модели 11
3. Модель системы 13
4. Требования и спецификации к системе 18
5. Верификация и анализ контрпримеров 20
6. Заключение 25
Список литературы 26
Компьютерные программы часто содержат различные ошибки. Еще Эдсгер Вибе Дейкстра говорил, что тестирование не позволяет обнаружить все ошибки. Особенно трудно тестировать параллельные, распределенные и многопоточные программы. Даже в тех случаях, когда функционирование каждой из взаимодействующих параллельных частей системы полностью ясно, человеку тяжело осознать работу параллельной системы целиком. Параллельные системы, на первый взгляд, работающие правильно, могут содержать ошибки, проявляющиеся в очень редких случаях (тупики, гонки [24] и т.д.). Существует множество примеров, когда из-за редко проявляющихся ошибок в сложных системах, прошедших тщательное тестирование, компании понесли огромные потери или пострадали пользователи1 [21].
В современном мире имеется большое количество автоматических систем, например автопилот в самолете или спутник, и критически важна корректная и безотказная работа всех компонентов таких систем. Поэтому на первый план выходят свойства надежности и предсказуемости поведения системы. Таким образом, формальная верификация программного кода, позволяющая существенно повысить качество системы, становится важнейшей областью научных исследований в информатике. Формальной верификацией программы, согласно [21], будем называть приемы и методы формального доказательства (или опровержения) того, что модель программной системы удовлетворяет заданной формальной спецификации (см. рис. 1).
Рис. 1: Общая схема верификации
Уже сейчас верификация является промышленным стандартом в критических областях, связанных как с дорогостоящими проектами, так и с человеческими жизнями [4]. С помощью формальной верификации можно доказать некоторые важные свойства системы, гарантировав отсутствие ошибок определенного типа и правильное функционирование системы. Это происходит за счет того, что верификация позволяет провести исчерпывающую проверку всех возможных вычислений модели системы, обнаруживая редко проявляющиеся ошибки [20], которые очень сложно проверить тестированием. Важно понимать, что проведя формальную верификацию и тестирование, нельзя гарантировать полное отсутствие ошибок в системе. Но при использовании этих методов вместе существенно повышается уровень доверия к системе.
На сегодняшний день для верификации сложных параллельных, многопоточных систем зарекомендовал себя метод проверки модели (model checking) [21]. Это метод проверки того, что данная формальная модель системы удовлетворяет ограничению, поставленному чаще всего в терминах какой-либо темпоральной логики, то есть логики, в которой истинность логических утверждений зависит от времени.
Важной частью автоматических систем являются роботы. Программное обеспечение для них часто относится к классу так называемых реагирующих систем, то есть систем, основная функция которых является поддержанием взаимодействия с окружением, а не преобразование информации. Такие системы могут бесконечно работать, они контролируют окружение, реагируя на внешние события. Вычисления на таких системах задаются бесконечной последовательностью состояний во времени. И именно с помощью формальной верификации возможно проанализировать все возможные вычисления таких систем.
В рамках Межвузовской Проектной Лаборатории Робототехники создают программную часть для контроллера робототехнического конструктора TRIK [13]. На таком контроллере, помимо операционной системы, запущено окружение времени выполнения [16], предоставляющее интерфейс программирования приложений для программирования робота, используя язык C++ с инструментарием Qt2 или скриптовый язык Qt Script3, позволяющее исполнять на роботе скрипты, а также управлять роботом извне. Скриптовый язык упрощает программирование роботов, однако окружение времени выполнения является многопоточной, параллельной программой, что обуславливает высокую сложность обнаружения ошибок. Такие роботы могут использоваться как автоматические системы. И безошибочное функционирование окружения времени выполнения в таких случаях является важной задачей. Отметим, что сама программа, окружение времени выполнения, написана на языке C++ с помощью инструментария Qt.
Таким образом, в нашем случае наиболее подходящим методом для формальной верификации окружения времени выполнения робототехнической системы является метод проверки модели. В классическом виде наиболее трудоемкой частью данного метода является разработка самой модели окружения времени выполнения [21]. Сложность связана с большим размером программы и постоянно возникающей при моделировании проблемой комбинаторного взрыва [23]. Необходимо также описать в терминах темпоральной логики интересующие свойства данной программы. Остальная часть работы, связанная с проверкой свойств на модели, выполняется автоматизировано с помощью соответствующих инструментов верификации.
В данной работе были достигнуты следующие результаты.
• Построена документированная, корректная и адекватная модель верифицируемой системы на языке PROMELA.
• Сформулированы требования на естественном языке и разработаны спецификации к системе на языке LTL на основе ожидаемого поведения исходной системы.
• Проведена верификация с помощью инструмента SPIN, найдены тринадцать ошибок и одно предупреждение.
• В качестве побочного результата при построении модели были найдены шесть недочетов, не связанных с процессом формальной верификации.
Исходный код модели, трассы контрпримеров и комментарии к ним выложены в открытый доступ [10].
Смоделированные компоненты и примитивы инструментария Qt могут быть использованы в других моделях. Модель документирована и может эволюционировать вместе с разработкой исходной программы окружения времени выполнения. Ввиду непредвиденно большого объема работы по анализу контрпримеров, не были доказаны некоторые существенные свойства системы. В качестве возможного продолжения работы существует две идеи:
• продолжить формальное доказательство свойств системы для текущей модели;
• в процессе моделирования большинство системных вызов не были учтены, к примеру, в модели практически полностью игнорируется взаимодействие окружения с драйверами датчиков робота; применение активно развивающегося подхода software model checking видится перспективным для решения этой проблемы.
