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

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

Современная жизнь неотрывно связана с различными техническими и информационными системами, которые обслуживают самые разнообразные сферы деятельности человека. В связи с этим всё большую важность приобретают проблемы валидации таких систем с целью устранения ошибок. Устранение ошибок на этапе проектирования системы позволяет зачастую не только сэкономить финансовые ресурсы, но и не подвергать риску здоровье и жизни людей, поэтому особое значение имеют методы формальной верификации, одним из которых является метод проверки модели (Model Checking).
В рамках выпускной квалификационной работы был разработан тестовый пример системы для верификатора PAT: были изучены и описаны теоретические сведения о видах верификации, основы линейной темпоральной логики; особое внимание было уделено методу Model Checking; был произведен сравнительный анализ существующих инструментов верификации, использующих этот метод, на основе которого был выбран наиболее подходящий инструмент проверки модели - PAT; разработана модель системы «Электрическая плита»; сформулированы требования к системе «Электрическая плита»; описана модель и требования к ней с помощью выбранного инструмента проверки моделей PAT; а также проведена верификация построенной модели системы «Электрическая плита» в данном инструменте.
Результаты этой работы могут использоваться в качестве учебно-методического обеспечения на дисциплинах «Теория автоматов и формальных языков», «Верификация программного обеспечения». Методические указания для проведения занятия на тему «Верификация автоматных программ с помощью верификатора PAT» представлены в ПРИЛОЖЕНИИ Б.
Результаты работы докладывались и обсуждались на XVI международной научно-практической конференции «Проблемы управления в социально-экономических и технических системах» в секции «Управление в технических системах». Работа была отмечена дипломом 3 степени [38].

Купить