Помощь студентам в учебе
ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ НА ЯЗЫКЕ PROMELA
|
ВВЕДЕНИЕ 4
1 Необходимые теоретические сведения 6
1.1 Конечный автомат и граф переходов 6
1.2 Применение автоматного подхода к программированию 7
1.3 Описание принципа моделирования системы 9
1.4 Валидация систем и формальная верификация 10
1.5 Метод Model Checking 12
1.6 Темпоральная логика 13
2 Выбор средств для верификации системы 16
2.1 Выбор метода подхода к проверке модели 16
2.2 Выбор утилиты для верификации модели. Верификатор SPIN и язык
Promela 17
2.3 Выбор графического интерфейса для работы с верификатором SPIN. .. 21
2.3.1 GUI Tau 22
2.3.2 GUI iSpin 23
2.3.3 GUI jSpin 25
2.3.4 GUI xSpin 27
3 Система «Кофейный автомат» 28
3.1 Модель системы «Кофейный автомат» 28
3.2 Требования к системе «Кофейный автомат». Спецификация LTL-
формул 30
4 Реализация и верификация системы 33
4.1 Реализация системы и требований к ней на языке Promela 33
4.1.1 Синтаксис языка Promela 33
4.1.2 Реализация модели системы «Кофейный автомат» на языке Promela
37
4.2 Верификация требований в SPIN. Работа с GUI iSpin 39
4.2.1 Работа с GUI iSpin. Режим симуляции 39
4.2.2 Работа с GUI iSpin. Режим верификации 46
4.3 Автомат Бюхи 56
ЗАКЛЮЧЕНИЕ 61
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ 63
ПРИЛОЖЕНИЕ
1 Необходимые теоретические сведения 6
1.1 Конечный автомат и граф переходов 6
1.2 Применение автоматного подхода к программированию 7
1.3 Описание принципа моделирования системы 9
1.4 Валидация систем и формальная верификация 10
1.5 Метод Model Checking 12
1.6 Темпоральная логика 13
2 Выбор средств для верификации системы 16
2.1 Выбор метода подхода к проверке модели 16
2.2 Выбор утилиты для верификации модели. Верификатор SPIN и язык
Promela 17
2.3 Выбор графического интерфейса для работы с верификатором SPIN. .. 21
2.3.1 GUI Tau 22
2.3.2 GUI iSpin 23
2.3.3 GUI jSpin 25
2.3.4 GUI xSpin 27
3 Система «Кофейный автомат» 28
3.1 Модель системы «Кофейный автомат» 28
3.2 Требования к системе «Кофейный автомат». Спецификация LTL-
формул 30
4 Реализация и верификация системы 33
4.1 Реализация системы и требований к ней на языке Promela 33
4.1.1 Синтаксис языка Promela 33
4.1.2 Реализация модели системы «Кофейный автомат» на языке Promela
37
4.2 Верификация требований в SPIN. Работа с GUI iSpin 39
4.2.1 Работа с GUI iSpin. Режим симуляции 39
4.2.2 Работа с GUI iSpin. Режим верификации 46
4.3 Автомат Бюхи 56
ЗАКЛЮЧЕНИЕ 61
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ 63
ПРИЛОЖЕНИЕ
На настоящий момент, функционирование современных систем опирается на сложные модели, зависящие от таких параметров, как распределённость и параллельность. Для систем реального времени наиболее важными являются такие характеристики, как управление временем и структура (модель) самой системы.
Традиционный способ тестирования систем ориентирован на разработку тестовых наборов, которые представляют собой входные воздействия и ожидаемые реакции. Такая проверка систем, особенно для распределённых систем реального времени, становится всё более ненадежной из-за большой сложности воспроизведения ситуаций, которые приводят именно к конкретным ожидаемым реакциям. В связи с этим, для обеспечения полноты проверки современных распределённых систем, используется формальная верификация. Данный способ проверки систем позволяет обеспечить гарантию того, что системы будут соблюдать свои ключевые свойства для всех путей исполнения заданной модели.
За последнее десятилетие такой метод формальной верификации, как поверка модели, преимущественно используется в проверке свойств не только современных распределённых систем, но и систем высокой надёжности, таких как медицинские системы или системы в космической сфере.
Поскольку зачастую проведение формальной верификации вручную является чересчур трудозатратным, то для этого используются многообразные утилиты, которые применяют различные способы и подходы для проверки моделей систем.
Для проведения формальной верификации (и, соответственно, выполнения проверки моделей) важно не только правильно построить модель тестируемой системы, но и корректно описать требования к модели, так как это влияет на правильность и адекватность поведения системы, а, соответственно, на корректность работы программ, разработанных на основе её модели.
Поэтому целью данной работы является разработка тестового примера для верификации автоматных программ на основе метода проверки модели. Для достижения данной цели были поставлены следующие основные задачи:
- изучить теоретические сведения об автоматном подходе к программированию;
- изучить принципы моделирования систем;
- изучить теоретические сведения о формальной верификации;
- изучить основы темпоральной логики;
- выбрать средства для верификации системы (метод подхода к проверке модели, утилиты для верификации и графического интерфейса - для работы с верификатором);
- разработать модель системы «Кофейный автомат»;
- сформулировать требования к системе «Кофейный автомат»;
- реализовать систему и требования к ней на языке верификатора;
- провести верификацию модели системы «Кофейный автомат».
Данная выпускная квалификационная работа состоит из введения, четырёх глав, заключения и трёх приложений.
Во введении отражена актуальность выпускной квалификационной работы, её цели и задачи. В первом разделе приводятся теоретические сведения о методах и технологиях, использованных в данной работе. Во втором разделе производится анализ и сравнение аналогичных продуктов, производится выбор необходимых продуктов и технологий. В третьем разделе описано моделирование системы «Кофейный автомат» и составление требований к ней для последующей верификации. В четвёртом разделе описывается процесс верификации системы. Заключение включает основные выводы по работе и планируемые перспективы развития. В приложения вынесены листинг программы, фрагмент результата верификации и методические рекомендации.
Традиционный способ тестирования систем ориентирован на разработку тестовых наборов, которые представляют собой входные воздействия и ожидаемые реакции. Такая проверка систем, особенно для распределённых систем реального времени, становится всё более ненадежной из-за большой сложности воспроизведения ситуаций, которые приводят именно к конкретным ожидаемым реакциям. В связи с этим, для обеспечения полноты проверки современных распределённых систем, используется формальная верификация. Данный способ проверки систем позволяет обеспечить гарантию того, что системы будут соблюдать свои ключевые свойства для всех путей исполнения заданной модели.
За последнее десятилетие такой метод формальной верификации, как поверка модели, преимущественно используется в проверке свойств не только современных распределённых систем, но и систем высокой надёжности, таких как медицинские системы или системы в космической сфере.
Поскольку зачастую проведение формальной верификации вручную является чересчур трудозатратным, то для этого используются многообразные утилиты, которые применяют различные способы и подходы для проверки моделей систем.
Для проведения формальной верификации (и, соответственно, выполнения проверки моделей) важно не только правильно построить модель тестируемой системы, но и корректно описать требования к модели, так как это влияет на правильность и адекватность поведения системы, а, соответственно, на корректность работы программ, разработанных на основе её модели.
Поэтому целью данной работы является разработка тестового примера для верификации автоматных программ на основе метода проверки модели. Для достижения данной цели были поставлены следующие основные задачи:
- изучить теоретические сведения об автоматном подходе к программированию;
- изучить принципы моделирования систем;
- изучить теоретические сведения о формальной верификации;
- изучить основы темпоральной логики;
- выбрать средства для верификации системы (метод подхода к проверке модели, утилиты для верификации и графического интерфейса - для работы с верификатором);
- разработать модель системы «Кофейный автомат»;
- сформулировать требования к системе «Кофейный автомат»;
- реализовать систему и требования к ней на языке верификатора;
- провести верификацию модели системы «Кофейный автомат».
Данная выпускная квалификационная работа состоит из введения, четырёх глав, заключения и трёх приложений.
Во введении отражена актуальность выпускной квалификационной работы, её цели и задачи. В первом разделе приводятся теоретические сведения о методах и технологиях, использованных в данной работе. Во втором разделе производится анализ и сравнение аналогичных продуктов, производится выбор необходимых продуктов и технологий. В третьем разделе описано моделирование системы «Кофейный автомат» и составление требований к ней для последующей верификации. В четвёртом разделе описывается процесс верификации системы. Заключение включает основные выводы по работе и планируемые перспективы развития. В приложения вынесены листинг программы, фрагмент результата верификации и методические рекомендации.
Формальная верификация играет ключевую роль в процессе разработки программного обеспечения, так как при данном способе обеспечивается достаточно полная проверка модели с помощью математических алгоритмов.
Формальная верификация позволяет устранять дефекты и обеспечивать качество и надёжность программного обеспечения, выявлять наиболее критичные подверженные ошибкам части создаваемой системы, производить оценку качества программного обеспечения. Особенно актуальным это является в ряде областей, где последствия ошибки в системе могут оказаться чрезвычайно дорогими (например, медицина или самолетостроение), так как формальная верификация способна обнаруживать сложные ошибки, которые сложно выявить с помощью других методов, таких как экспертиза или тестирование.
В ходе выполнения выпускной квалификационной работы была достигнута цель - разработан тестовый пример для верификации автоматных программ и решены поставленные задачи, а именно:
- изучены теоретические сведения об автоматном подходе к программированию;
- изучены принципы моделирования систем;
- изучены теоретические сведения о формальной верификации;
- изучены основы темпоральной логики;
- выбраны средства для верификации системы (метод подхода к проверке модели, утилиты для верификации и графического интерфейса - для работы с верификатором);
- разработана модель системы «Кофейный автомат»;
- сформулированы требования к системе «Кофейный автомат»;
- реализована система и требования к ней на языке верификатора (Promela);
- проведена верификация модели системы «Кофейный автомат» с помощью верификатора SPIN.
Результаты данной работы докладывались и обсуждались на Международной научно-практической конференции «Проблемы управления в социально-экономических и технических системах» (2018 г., доклад:
«Моделирование работы кофейного автомата»), Международной научно-практической конференции «Проблемы управления в социально¬
экономических и технических системах» (2019 г., доклад: «Проверка модели программы с помощью логики LTL», работа отмечена дипломом II степени), VI Международной научной конференции «Проблемы управления, обработки и передачи информации (УОПИ-2018)» (2018 г., доклад: «Моделирование работы кофейного автомата»), Международной научно-практической конференции «Current Trends in History, Culture, Science and Technology» / «Современные направления в истории, культуре, науке и технике» (2019 г., доклад: «Simulation of the coffee vending machine work»), научном стендапе «Эпоха Гагарина: вызовы и приоритеты» в рамках Гагаринской недели (2019 г., тема
выступления: «Верификация автоматных программ»).
Статьи по данной работе были опубликованы в сборниках [13, 14, 21, 22].
Также, по данной работе были разработаны методические рекомендации по теме: «Верификация автоматных программ в верификаторе SPIN с помощью графического интерфейса GUI iSpin» (Приложение В).
Формальная верификация позволяет устранять дефекты и обеспечивать качество и надёжность программного обеспечения, выявлять наиболее критичные подверженные ошибкам части создаваемой системы, производить оценку качества программного обеспечения. Особенно актуальным это является в ряде областей, где последствия ошибки в системе могут оказаться чрезвычайно дорогими (например, медицина или самолетостроение), так как формальная верификация способна обнаруживать сложные ошибки, которые сложно выявить с помощью других методов, таких как экспертиза или тестирование.
В ходе выполнения выпускной квалификационной работы была достигнута цель - разработан тестовый пример для верификации автоматных программ и решены поставленные задачи, а именно:
- изучены теоретические сведения об автоматном подходе к программированию;
- изучены принципы моделирования систем;
- изучены теоретические сведения о формальной верификации;
- изучены основы темпоральной логики;
- выбраны средства для верификации системы (метод подхода к проверке модели, утилиты для верификации и графического интерфейса - для работы с верификатором);
- разработана модель системы «Кофейный автомат»;
- сформулированы требования к системе «Кофейный автомат»;
- реализована система и требования к ней на языке верификатора (Promela);
- проведена верификация модели системы «Кофейный автомат» с помощью верификатора SPIN.
Результаты данной работы докладывались и обсуждались на Международной научно-практической конференции «Проблемы управления в социально-экономических и технических системах» (2018 г., доклад:
«Моделирование работы кофейного автомата»), Международной научно-практической конференции «Проблемы управления в социально¬
экономических и технических системах» (2019 г., доклад: «Проверка модели программы с помощью логики LTL», работа отмечена дипломом II степени), VI Международной научной конференции «Проблемы управления, обработки и передачи информации (УОПИ-2018)» (2018 г., доклад: «Моделирование работы кофейного автомата»), Международной научно-практической конференции «Current Trends in History, Culture, Science and Technology» / «Современные направления в истории, культуре, науке и технике» (2019 г., доклад: «Simulation of the coffee vending machine work»), научном стендапе «Эпоха Гагарина: вызовы и приоритеты» в рамках Гагаринской недели (2019 г., тема
выступления: «Верификация автоматных программ»).
Статьи по данной работе были опубликованы в сборниках [13, 14, 21, 22].
Также, по данной работе были разработаны методические рекомендации по теме: «Верификация автоматных программ в верификаторе SPIN с помощью графического интерфейса GUI iSpin» (Приложение В).