Пояснительная записка к выпускной квалификационной работе




НазваниеПояснительная записка к выпускной квалификационной работе
страница1/9
Дата публикации17.03.2013
Размер0.68 Mb.
ТипПояснительная записка
odtdocs.ru > Информатика > Пояснительная записка
  1   2   3   4   5   6   7   8   9
Министерство образования и науки Российской Федерации

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


Факультет Информационных технологий и программирования

Направление (специальность) прикладная математика и информатика

Квалификация (степень) бакалавр прикладной математики и информатики

Специализация -----------------------

Кафедра Компьютерных технологий Группа 4538

ПОЯСНИТЕЛЬНАЯ ЗАПИСКА

^ К ВЫПУСКНОЙ КВАЛИФИКАЦИОННОЙ РАБОТЕ

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


Автор квалификационной работы Егоров К.В. (подпись)
Руководитель Шалыто А.А. (подпись)


^ К ЗАЩИТЕ ДОПУСТИТЬ

Зав. кафедры Васильев В.Н. (подпись)
« » 2008 г.


Санкт-Петербург, 2008 г.

Квалификационная работа выполнена с оценкой
Дата защиты « » 2008 г.
Секретарь ГАК
Листов хранения
Чертежей хранения

Содержание

Введение 5

ГЛАВА 1. Автоматное программирование и верификация автоматов 9

1.1. Автоматное программирования 9

1.1.1. Switch-технология 9

1.1.2. Инструментальное средство UniMod 12

1.2. Традиционная верификация моделей на основе метода
Model Checking 14

1.2.1. Представление модели 14

1.2.2. Временная логика LTL 17

1.2.3. Построение автомата Бюхи по LTL формуле 18

1.2.4. Проверка пустоты пересечения языков 19

1.3. Существующие верификаторы, основанные на автоматном подходе 22

1.3.1. Spin 22

1.3.2. Bogor 23

1.4. Особенности автоматных программ 23

Выводы по главе 1 24

ГЛАВА 2. Обзор методов верификации автоматных программ 26

2.1. Представление автоматной модели 26

2.2. Язык LTL для описания поведения автоматных программам 28

2.3. Особенности верификации автоматных программ 30

2.4. Верификация автоматных программ на многоядерном компьютере 32

2.4.1. Расширение верификатора Spin для многоядерного компьютера 33

Выводы по главе 2 34

ГЛАВА 3. Методика верификации автоматных программ 36

3.1. Параллельная верификация автоматных программ 36

3.2. Методика верификации автоматных программ 39

Выводы по главе 3 43

ГЛАВА 4. Описание верификатора 44

4.1. Описание основных классов верификатора 44

4.2. Применение основных классов верификатора 46

4.2.1. Построение модели автоматной программы 46

4.2.2. Построение LTL формул 47

4.2.3. Трансляция LTL формулы в автомат Бюхи 49

4.2.4. Верификация модели автоматной программы 49

Выводы по главе 4 51

ГЛАВА 5. Верификация автоматных программ 53

5.1. Пример верификации модели автоматной программы 53

5.2. Анализ работы верификатора на примере игры «Побег» 56

5.2.1. Анализ модели игрового мира 57

5.2.2. Верификация тактик полицейских машин 61

5.3. Верификация модели банкомата 62

5.3.1. Результат верификации модели банкомата 63

5.3.2. Пример верификации модели банкомата по методике верификации автоматных программ 66

5.4. Анализ эффективности верификации на многоядерном компьютере 69

Выводы по главе 5 71

Заключение 73

Литература 74

Введение


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

Проверке качества программного обеспечения (ПО) ответственных систем, казалось бы, должно было уделяться значительное внимание, но до недавнего времени это было не так, о чем свидетельствуют многочисленные катастрофы. Так, одна из самых дорогих катастроф произошла 4 июня 1996 года во время первого запуска новой ракеты-носителя Ариан-5, разработанной Европейским космическим агентством. Запуск прошел неудачно – ракета самоуничтожилась через 37 с после старта из-за неверной работы бортового ПО. Эта неудача произошла по причине ошибки преобразования 64-битного числа с плавающей запятой в 16-битное целое. Такое упущение привело к потере 800 миллионов долларов.

К сожалению, отечественное освоение космоса также не обошлось без инцидентов, произошедших по вине ПО. «В начале 70 годов прошлого столетия между СССР и США разгоралась космическая гонка, кто первым совершит мягкую посадку на Марс. Советскую марсианскую программу преследовали хронические неудачи. Из целой армады межпланетных станций только одной удалось совершить мягкую посадку, однако ни одной фотографии аппарат так и не передал. Оказывается, на аппараты марсианской серии впервые были установлены бортовые цифровые ЭВМ»1. Первый полет прошел неудачно – на траекторию полета к Марсу станция не перешла по причине ввода в вычислительную бортовую машину ошибочного значения времени запуска двигателя. Из-за ошибки в разряде, двигатель должен был запуститься не через несколько десятков минут, как предусматривала программа полета, а через полторы сотни часов. Второй полет также не принес никакой научной ценности из-за ошибки бортового компьютера. Хотя аппарат и смог добраться до Марса, однако мягкая посадка не была осуществлена. Последняя неудача была уже в 1989 году, когда станция Фобос-2 не смогла выполнить поставленную задачу. Наиболее вероятная причина отказа: «одновременное «зависание» двух каналов бортовой ЦВМ и, как следствие, потеря ориентации и закрутка аппарата с остаточными на этапах разворотов угловыми скоростями»2.

Одним из основных методов проверки программы на наличие ошибок является тестирование. На практике оно применяется в большинстве случаев. Однако «тестирование позволяет показать наличие ошибок, но не их отсутствие»3. При таком подходе к проверке, можно удостовериться в правильности работы программы только при определенном ее поведении или каком-то конечном числе входных данных. Однако существуют ошибки, которые могут появляться крайне редко, особенно при параллельном исполнении программы. Поэтому, для того чтобы исключить возможность их появления, требуется рассмотреть все возможные варианты поведения системы, что невозможно.

Формальная верификация – метод проверки того, что программа соответствует спецификации, который основан на строгих математических принципах. При таком подходе используется логический формализм и математическое описание модели. Автоматическая верификация – это формальная верификация, проводимая машиной без вмешательства человека. Далее в работе под словом «верификация» будет пониматься автоматическая верификация.

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

Цель настоящей работы состоит в создании верификатора для модели автоматных программ, созданных при помощи инструментального средства UniMod [1, 2]. Особенности этого класса программ позволяют избежать первой части верификации – построение модели, так как каждая такая программа уже представляет собой модель, пригодную для проверки определенных утверждений о ней без ее модификации. Требования к программе будем формулировать в виде формул темпоральной логики LTL (Linear Time Logic).

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

Для создания нового верификатора необходимо разработать собственное представление модели, которая не использует внутреннее представление модели в инструментальном средстве UniMod. Это было сделано для того, чтобы и при создании новых средств для написания программ в рамках автоматного программирования можно было бы применять данный верификатор. При этом необходимо рассмотреть применимость для автоматных программ алгоритмов верификации при использовании логики LTL. Это уже рассматривалось в работе [3], но для уже имеющихся верификаторов.

В связи с ростом числа ядер персональных компьютеров, возникает задача распараллеливания процесса верификации автоматных программ. Поэтому еще одна задача работы – создание верификатора, который мог бы равномерно распределять нагрузку на ядра и работал бы эффективнее на многоядерном компьютере по сравнению с одноядерным.
  1   2   3   4   5   6   7   8   9

Добавить документ в свой блог или на сайт

Похожие:

Выпускной квалификационной работы
Разработка и исследование трёхфазного инвертора напряжения с использованием промежуточного высокочастотного преобразования

Пояснительная записка к курсовой работе принцип

Пояснительная записка Учебный план для 1 классов моу «Средняя общеобразовательная школа №4»
Пояснительная записка

Пояснительная записка Учебный план для 1-2 классов моу «Средняя общеобразовательная школа №4»
Пояснительная записка

Пояснительная записка к курсовой работе по дисциплине «Теория Автоматов»

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

Положение о выпускной квалификационной работе (вкр) студента Тамбовского...
Настоящее положение разработано на основе Письма Министерства образования РФ от 10 июля 1998 г. №12-52-111 ин/12-23 «Рекомендации...

Пояснительная записка к лабораторной работе по дисциплине «Конструкторское...
В работе разработана принципиальная схема и печатная плата четырёхразрядного регистра сдвига с параллельной записью. Устройство разрабатывается...

Пояснительная записка к курсовой работе хранилища и распределенные базы данных

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

Вы можете разместить ссылку на наш сайт:
Школьные материалы


При копировании материала укажите ссылку © 2013
контакты
odtdocs.ru
Главная страница