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

Разработка верификатора автоматных программ

© 2008 г. К. В. Егоров
Научные руководители: А. А. Шалыто

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

Бакалаврская работа
Исходные коды
Исходные тексты
Презентация

Аннотация

Цель работы - разработка верификатора автоматных программ, написанных при помощи инструментального средства UniMod. Верификатор позволяет проверять утверждения о моделях автоматных программ. Каждая такая модель представляется в виде XML-файла, созданного инструментальным средством UniMod. Требования к программам записываются на языке логики линейного времени (Linear Time Logic, LTL).

Особенностью созданного верификатора является его специализация на проверке утверждений о моделях автоматных программ. Благодаря этому, верифицируется модель автоматной программы, а не ее представление, описанное с помощью входного языка верификатора, как это делается традиционно при использовании метода Model Checking. Также в работе был реализован алгоритм распараллеливания процесса верификации, который позволяет уменьшить время верификации на многоядерном компьютере.