УНИВЕРСИТЕТ ИТМО
Кафедра «Технологии программирования»

Введение в верификацию автоматных программ на основе метода Model checking

© 2006 С. Э. Вельдер, А. А. Шалыто

Санкт-Петербургский государственный институт информационных технологий, механики и оптики

Документация

Аннотация

Верификация моделей – это набор идей и методов для построения моделей работающих программ, математической формулировки требований к ним, отражающих правильность их работы, и создания алгоритмов для формальной проверки выполнения этих требований.

В настоящей работе основное внимание концентрируется на особой технике верификации, которая базируется на так называемых темпоральных логиках и называется Model checking. Такая техника позволяет проверять динамические свойства программ, например, последовательность, в которой достигаются определенные их состояния.

Кратко сформулируем основные достоинства автоматных программ в части их верификации:

• класс автоматных программ является наиболее удобным для верификации методом Model checking, так как в этом случае модель программы может быть автоматически построена по спецификации ее поведения, задаваемой в общем случае системой взаимодействующих конечных автоматов, в то время как для программ других классов модель приходится строить вручную;

• структура автоматных программ, в которых функции входных и выходных воздействий почти полностью отделены от логики программ, делает практичным верификацию этих функций на основе формальных доказательств с использованием пред- и постусловий.

Изложение метода Model checking выполняется в три этапа:

1. Преобразование автомата Мили в модель Крипке и разработка требований к модели.

2. Верификация полученной модели и построение в ней сценариев, позволяющих разработчику проверить справедливость того или иного логического свойства модели.

3. Интерпретация сценария, полученного для модели Крипке, в исходном автомате Мили.

Применение этого метода в работе демонстрируется на примере программы для «Универсального инфракрасного пульта для бытовой техники» (http://is.ifmo.ru/projects/irrc/).