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



Главная

Новости
 Новости науки
 Важное
 Почетные доктора
 Инновации
 Культура
 Люди
 Разное
 Скартел-Yota
 Стрим
 Смольный
Учебный процесс
 Образование
 Дипломы
 Курсовые проекты
 Лабораторные работы
 Учебные курсы
 Визуализаторы
 Unimod-проекты
 Семинары
 Стипендии
Наука
 События и факты
 Госконтракты
 Статьи
 Диссертации
 Книги
 Презентации
 Свидетельства
 Сотрудничество
Исследования
 Автоматы
 Верификация
 Биоинформатика
 Искусственный интеллект
 Генетические алгоритмы
 Движение
 UniMod
 Роботы и агенты
 Нейронные сети
 ФЦП ИТМО-Аалто
 Разное

О нас
 Премии
 Сертификаты и дипломы
 Соревнования по программированию
 Прорыв
 Автографы
 Рецензии

Беллетристика
 Мотивация
 Мысли
Медиа
 Видео
 Фотографии
 Аудио
 Интервью

English
 Home

 Articles
 Posters
 Automata-Based Programming
 Initiatives
 Projects
 Presentations
 UniMod
 UniMod Projects
 Visualizers


Поиск по сайту

Яndex



   Главная / Верификация / Введение в верификацию автоматных программ на основе метода Model checking (версия для печати)


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



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

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

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

Аннотация

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

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

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

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

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

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

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

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

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

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


© 2002—2017 По техническим вопросам сайта: vl.ulyantsev@gmail.com