РАЗРАБОТКА ТЕСТОВОГО ПРИМЕРА МОДЕЛИ ПРОГРАММЫ ДЛЯ ВЕРИФИКАТОРА PAT

ВВЕДЕНИЕ 3
Глава 1. Теоретические сведения 7
1.1 Методы валидации систем 7
1.2 Методы формальной верификации 8
1.3 Конечный автомат и автоматный подход 10
1.4 Описание метода Model Checking 13
1.5 Моделирование системы 15
1.6 Описание свойств модели 16
Глава 2. Сравнение и анализ инструментов проверки моделей 19
2.1 Сравнение инструментов проверки моделей 19
2.2 Результаты сравнительного анализа 28
Глава 3. Разработка модели электрической плиты 31
3.1 Описание модели системы управления электрической
плитой 31
3.2 Спецификация системы 33
Глава 4. Реализация и верификация 35
4.1 Описание работы в среде PAT 35
4.2 Верификация модели 46
ЗАКЛЮЧЕНИЕ 62
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ 64
ПРИЛОЖЕНИЕ А 68
ПРИЛОЖЕНИЕ Б
Купить

На настоящий момент аппаратные и программные системы занимают большое место в жизни человека. Общество всё больше зависит от программных и аппаратных систем, которые помогают нам практически во всех аспектах повседневной жизни. Часто мы можем даже не осознавать, что такие системы в это вовлечены. Некоторые функции управления в современных автомобилях основаны на встроенных программных решениях, например, торможение, подушки безопасности, круиз-контроль и так далее. Мобильные телефоны, системы связи, медицинские устройства, аудио- и видеосистемы и бытовая техника в целом содержат большое количество программного обеспечения. Кроме того, в системах транспорта, производства и управления всё шире применяются встроенные программные решения, обеспечивающие гибкость и экономичность. Выходит, что огромная ответственность “ложится на плечи” программ, которые управляют определёнными устройствами.
Следовательно, из-за постоянного роста автоматизации жизни всё более обостряется необходимость преждевременного обнаружения и устранения ошибок в программах. Это имеет большое значение, так как чем раньше ошибка будет обнаружена, тем меньше вреда она принесёт. В ряде приложений ошибки не критичны, например, в офисных приложениях или веб-сервисах. Они сводятся к лёгким моральным травмам пользователей и репутационным издержкам производителя ПО, эти ошибки достаточно легко обнаружить и выполнить восстановление системы, а также их возможно быстро исправить, например, выпустив патч, либо просто поправив код, например, веб¬сервиса на сервере. В таких случаях важнее не избавится от всех ошибок, а как можно быстрее вывести свой продукт на рынок. Но существует ряд систем с повышенными требованиями к надёжности, в которых ошибка в программе может принести вред как со стороны вопроса безопасности, так и с экономической: если ошибка, которая была допущена на этапе проектирования устройства, обнаружится только после старта производства, то появится необходимость в её исправлении уже не исключительно в проекте, но и во всех устройствах, которые были произведены. В истории описано большое количество случаев ошибок, которые привели к большим финансовым потерям. Один из таких случаев произошёл в июне 1996 года: французы запускали ракету Ariane-5, которая взорвалась спустя 40 секунд после старта из-за неверной работы бортового программного обеспечения. На разработку ракеты было потрачено 7 млрд. долларов, ущерб от потери ракеты составил примерно 500 млрд. долларов. Кроме экономической стороны, ошибка в работе систем с повышенными требованиями к надёжности может даже причинить вред здоровью людей, и даже иметь летальные последствия. Примером такой ошибки может быть случай, который произошёл в Саудовской Аравии. В феврале 1991 года ракетный комплекс Patriot не смог перехватить ракету Scud. ЗРК, прикрывавший авиабазу, увидел ракету, но не сумел попасть в нее из-за ошибки в собственном математическом обеспечении. Из-за особенностей хранения чисел в системе опорное значение времени при округлении искажалось, что накапливало рассогласование примерно на треть секунды за 100 часов непрерывной работы комплекса. Ракета попала на американскую авиабазу. Взрыв убил 28 человек и около сотни получили ранения. Ошибка эта была уже известна до момента трагедии, но из-за начавшейся войны обновить ПО просто не успевали. Носители с «патчем» прибыли только на следующий день после ракетного удара.
Хочется уточнить, что системы с повышенными требованиями к надёжности это не только спутники, самолёты и т.п. Это в том числе системы, в которых:
- затруднено исправление ошибок (потребительская электроника);
- велик масштаб использования (та же потребительская электроника, важные веб-сервисы, которыми пользуются миллионы человек);
- высокая степень доверия человека.
Именно поэтому, так как возрастают размеры и сложности аппаратных и программных систем, необходимо обеспечить процесс валидации систем с использованием методов и инструментов, которые могут облегчить автоматический анализ корректности. Кроме того, верификация системы, исправление ошибок на этапе ее проектирования экономически целесообразно, позволяя экономить время и средства на производство некорректно работающей системы. В то время как тестирование ручным способом не только зачастую не способно обеспечить полной проверки, но и требует наличия уже готового, произведенного продукта.
Поэтому важно изучать методы формальной верификации моделей систем, позволяющей на этапе проектирования производить валидацию модели.
Целью данной работы является разработка тестового примера системы для верификации на основе Model Checking (метода проверки модели). Для достижения данной цели были поставлены следующие задачи:
- описать теоретические сведения о формальной верификации и основах темпоральной логики;
- сравнить существующие инструменты верификации, использующие данный метод;
- на основе полученных данных выбрать наиболее подходящий;
- разработать модель системы «Электрическая плита»;
- сформулировать требования к системе «Электрическая плита»;
- описать модель и требования к ней с помощью выбранного инструмента проверки моделей;
- провести верификацию в выбранном инструменте на построенной модели системы «Электрическая плита».
Данная работа состоит из четырёх глав. В первой главе рассказывается о методах валидации систем, особое внимание уделяется автоматному подходу и методу проверки моделей. Во второй главе производится анализ и сравнение инструментов, использующих метод проверки моделей. На основе анализа происходит выбор необходимого инструмента. В третьей главе описывается моделирование системы «Электрическая плита» и составление требований к ней на языке линейной темпоральной логики для последующей верификации. В четвёртой главе описывается процесс реализации модели и спецификации в PAT и верификация модели для описанных требований.
Купить