Тема: Формальная верификация окружения времени выполнения робототехнической системы

Компьютерные программы часто содержат различные ошибки. Еще Эдсгер Вибе Дейкстра говорил, что тестирование не позволяет обна­ружить все ошибки. Особенно трудно тестировать параллельные, рас­пределенные и многопоточные программы. Даже в тех случаях, когда функционирование каждой из взаимодействующих параллельных ча­стей системы полностью ясно, человеку тяжело осознать работу парал­лельной системы целиком. Параллельные системы, на первый взгляд, работающие правильно, могут содержать ошибки, проявляющиеся в очень редких случаях (тупики, гонки [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 видится перспективным для решения этой проблемы.
Купить