Бакалаврская работа
Исходные коды
Исходные тексты Презентация
© 2008 г. К. В. Егоров
Научные руководители: А. А. Шалыто
Санкт-Петербургский государственный университет информационных технологий, механики и оптики
Бакалаврская работа
Исходные коды
Исходные тексты
Презентация
Цель работы - разработка верификатора автоматных программ, написанных при помощи инструментального средства UniMod. Верификатор позволяет проверять утверждения о моделях автоматных программ. Каждая такая модель представляется в виде XML-файла, созданного инструментальным средством UniMod. Требования к программам записываются на языке логики линейного времени (Linear Time Logic, LTL).
Особенностью созданного верификатора является его специализация на проверке утверждений о моделях автоматных программ. Благодаря этому, верифицируется модель автоматной программы, а не ее представление, описанное с помощью входного языка верификатора, как это делается традиционно при использовании метода Model Checking. Также в работе был реализован алгоритм распараллеливания процесса верификации, который позволяет уменьшить время верификации на многоядерном компьютере.