© 2006 С. Э. Вельдер, А. А. Шалыто
Санкт-Петербургский государственный институт информационных технологий, механики и оптики
Верификация моделей – это набор идей и методов для построения моделей работающих программ, математической формулировки требований к ним, отражающих правильность их работы, и создания алгоритмов для формальной проверки выполнения этих требований.
В настоящей работе основное внимание концентрируется на особой технике верификации, которая базируется на так называемых темпоральных логиках и называется Model checking. Такая техника позволяет проверять динамические свойства программ, например, последовательность, в которой достигаются определенные их состояния.
Кратко сформулируем основные достоинства автоматных программ в части их верификации:
класс автоматных программ является наиболее удобным для верификации методом Model checking, так как в этом случае модель программы может быть автоматически построена по спецификации ее поведения, задаваемой в общем случае системой взаимодействующих конечных автоматов, в то время как для программ других классов модель приходится строить вручную;
структура автоматных программ, в которых функции входных и выходных воздействий почти полностью отделены от логики программ, делает практичным верификацию этих функций на основе формальных доказательств с использованием пред- и постусловий.
Изложение метода Model checking выполняется в три этапа:
Преобразование автомата Мили в модель Крипке и разработка требований к модели.
Верификация полученной модели и построение в ней сценариев, позволяющих разработчику проверить справедливость того или иного логического свойства модели.
Интерпретация сценария, полученного для модели Крипке, в исходном автомате Мили.
Применение этого метода в работе демонстрируется на примере программы для «Универсального инфракрасного пульта для бытовой техники» (http://is.ifmo.ru/projects/irrc/).