Введение

Актуальность

Автоматное программирование, основанное на применении конечных автоматов, всё шире используется при разработке программного обеспечения (ПО). В частности, оно применяется для построения программ управления ответственными объектами, для которых особую важность имеет правильность их работы.

По данной теме проводятся исследования в России и за рубежом [6 - 40]. Настоящая работа является продолжением работ [20, 28, 32].

Цель диссертационной работы

Цель работы - разработка метода верификации автоматных программ. Для достижения этой цели в диссертации решаются следующие задачи:

• выбор математических моделей управляющих автоматов;

• разработка алгоритма построения Spin-модели управляющего автомата;

• разработка алгоритма построения Spin-модели системы вложенных управляющих автоматов (иерархического автомата);

• разработка алгоритма построения Spin-модели параллельно работающих иерархических автоматов;

• разработка метода верификации автоматных программ: построение Spin- модели, преобразование расширенных LTL-формул в Spin-формулы, преобразование контрпримера в путь в системе автоматов;

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

• разработка инструментального средства, поддерживающего предлагаемый метод.

Методы исследования

В работе использованы методы дискретной математики, построения и анализа алгоритмов, теории автоматов, теории верификации, объектно­ориентированного программирования.

Научная новизна

В работе получены следующие результаты, которые выносятся на защиту:

• обоснован выбор математических моделей управляющих автоматов;

• разработан алгоритм построения Spin-модели управляющего автомата;

• разработан алгоритм построения Spin-модели системы вложенных управляющих автоматов (иерархического автомата);

• разработан алгоритм построения Spin-модели параллельно работающих иерархических автоматов;

• разработан метод верификации автоматных программ: построение Spin- модели, преобразование расширенных LTL-формул в Spin-формулы, преобразование контрпримера в путь в системе автоматов;

• разработано инструментальное средство, поддерживающее предлагаемый метод;

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

• результаты работы внедрены в практику проектирования для сред с конечным и бесконечным числом состояний.

Достоверность

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

Практическое значение

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

На основе этого метода автором разработано инструментальное средство Stater, которое позволяет графически строить иерархические автоматы [41, 42,44, 45], импортировать их из сред для проектирования автоматных программ, генерировать по этим автоматам программный код и проводить верификацию автоматных программ.

Экспериментальные исследования

На примере задачи поиска пути с O(I)памяти на бесконечном клетчатом поле были выполнены экспериментальные исследования указанного выше инструментального средства. Исследования проводились на 800 автоматных программах, созданных при помощи генетического программирования. Удалось доказать корректность работы для 231 программы (вопрос о корректности остальных программ остаётся открытым).

Использование и внедрение результатов работы

Результаты работы использованы в ходе выполнения государственного контракта по теме «Разработка технологии верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода» (отчёт по I этапу «Выбор направления исследований и базовых методов» (2007, http://is.ifmo.ru/verification/_2007_01_report-verification.pdf), по II этапу «Теоретические исследования поставленных перед НИР задач» (2007, http://is.ifmo.ru/verification/_2007_02_report-verification.pdf), по III этапу «Экспериментальные исследования поставленных перед НИР задач» (2007, http://is.ifmo.ru/verification/_2007_03_report-verification.pdf), по IV этапу «Обобщение и оценка результатов исследований» (2007, http://is.ifmo.ru/verification/_2007_04_report-verification.pdf).

исследований при участии автора написана монография, опубликованная в издательстве «Наука» в 2011 году.

Результаты использованы также при проведении занятий по курсу «Верификация программного обеспечения» для магистрантов кафедры «Компьютерные технологии» в 2012/2013 и 2013/2014 учебных годах, что подтверждается соответствующим актом. Для поддержки этого курса в 2012 году в НИУ ИТМО было опубликовано учебное пособие [46]. Акт использования имеется.

Кроме того, по курсу при участии автора был создан учебно­методический комплекс, опубликованный в системе дистанционного обучения НИУ ИТМО. Там же опубликован его перевод на английский язык, выполненный автором [47]. Акт использования имеется.

Результаты работы внедрены в 2012 году в ООО «Специальный технологический центр» (Санкт-Петербург) при разработке редактора описания антенных систем, что подтверждается актом внедрения.

Результаты также внедрены в 2012 году в студии «PointOmega Games» (Санкт-Петербург) при разработке игры Turtleball HD (https://play.google.com/store/apps/details?id=com.pointomega.turtleball), что подтверждается актом внедрения.

Апробация диссертации

Основные положения диссертационной работы докладывались на следующих научных и научно-практических конференциях: Международная научно-методическая конференция «Высокие интеллектуальные технологии и инновации в образовании и науке» (СПбГПУ, 2008), Конференция молодых ученых ИТМО 2009, Всероссийская научная конференция по проблемам информатики СПИСОК (Матмех СПбГУ, 2011), Международная научно­практическая конференция Tools &Methods of Program Analysis (Костромской государственный технический университет, TMPA-2013), Haifa Verification Conference (Haifa, 2014).

Публикации

По результатам диссертации лично автором и в соавторстве опубликовано 11 научных работ, среди которых монография (издательство «Наука»), учебное пособие Университета ИТМО (на русском и английском языках), три статьи (все в изданиях из перечня ВАК).

Кроме того, автором получено свидетельство о регистрации программ на описываемое ниже инструментальное средство Converter.

Структура диссертации

Диссертация изложена на 185 страницах и состоит из введения, пяти глав, заключения и двух приложений. Список литературы состоит из 87 наименований. Работа иллюстрирована 34 рисунками и содержит четыре таблицы.

В первой главе приведён обзор существующих решений. Во второй главе приведены основные понятия. В третьей главе описан предлагаемый метод для разработки и верификации автоматных программ, а также описание разработанных автором инструментальных средств. Четвёртая глава содержит описание внедрения полученных результатов на практике. В пятой главе приведено описание подхода к верификации в случаях, когда модель внешней среды нельзя представить в виде автомата, например, для клетчатого поля неограниченных размеров. Подход продемонстрирован на примере доказательства корректности автоматных программ, решающих задачу о поиске пути с O(I)памяти.