Формальная спецификация и верификация. Задача о спящем парикмахере

Министерство образования и  науки Российской Федерации

Магнитогорский Государственный  Технический Университет им. Г.И.Носова

 

 

 

 

 

Кафедра вычислительной техники и  прикладной математики

 

 

 

 

 

 

 

Курсовая  работа

На тему: «Формальная спецификация и верификация.

Задача о спящем парикмахере»

 Дисциплина: «Теория вычислительных процессов»

 

 

 

 

 

 

 

 

 

 

 

 

   Выполнил:        ст.гр. АВБ-08

Коляда А. И.

 

Проверил:  Калитаев А.Н.                                                                    

 

 

 

 

 

 

 

 

 

 

 

Магнитогорск

2010 

Оглавление

 

Введение

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

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

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

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

 

1. Спецификация и верификация  программ

1. Общие сведения о спецификации программы

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

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

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

 

 

 

Рис. 1.1. Категории языков спецификации

 

Универсальные языки спецификации (VDM, Z, RAISE и др.) имеют общематематическую основу и следующие виды средств:

 

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

 

 

В VDM и RAISE нет средств описания графовых структур, управления и параллелизма, однако имеется механизм конструирования  новых структур данных.

 

Языки спецификации областей включают в себя следующие языки:

 

• спецификации доменов;
• описания взаимодействий;
• спецификации ЯП и трансляторов;
• спецификации БД и знаний;
• спецификации пакетов прикладных программ и др.

 

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

Язык спецификации доменов DSL (Domain Specific Language) представляет некоторое  подмножество языка программирования и специально средства для описания специальных проблем домена [6.14]. Он подразделяется на внешние и внутренние языки. Внешние языки (типа Unix, XML и др.) по уровню выше языка описания приложения. Описание в нем сводится к языку DSL специальными генераторами или текстовыми редакторами, трансформирующими абстрактные понятия домена к понятиям языка DSL. Внутренние языки (С, С++), а также языки Java, Smalltalk ограничены синтаксисом и семантикой основного базового языка программирования приложений.

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

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

 

Языки описания средств программирования включают в себя языки, основанные на равенствах и подстановках с операционной семантикой (Лисп, Рефал); логические языки; языки операций (АPL) над последовательностями и матрицами; табличные языки; сети, графы [6.5, 6.11]. Язык логики предикатов с набором базисных функций используется для записи пред- и постусловий, инвариантов.

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

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

Продукция или правила подстановки  общего вида – это λ → ρ где λ и ρ - произвольные слова в фиксированном алфавите. Нормальный алгоритм Маркова представляет собой упорядоченный набор правил, некоторые из них отмечены как завершающие. Применение правила λ → ρ к слову φ состоит в подстановке слова ρ вместо самого левого слова  λ в φ. Вычисление заканчивается, когда применяется завершающее правило, состоящее в порождении одного слова.

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

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

2. Верификация программ

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

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

 

Верификации подвергаются:

 

• тесты, тестовые процедуры и входные наборы данных.
• компоненты системы и их интерфейсы (программные, технические и информационные) и взаимодействия объектов (протоколы, сообщения) в распределенных средах;
• описание доступа к БД, средства защиты от несанкционированного доступа к данным разных пользователей;
• документация на систему.

1. Подходы к верификации моделей

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

 

Верификация объектных моделей  основывается на спецификации следующих  элементов:

 

1. Базовых (простых) объектов ОМ, атрибутами которых являются данные и операции объект функции над этими данными.
2. Проверенных объектов с помощью операций (функции), используемых в качестве теорем, а все операции, которые применяются над их подобъектами, не выводят их из множества состояний объектов.
3. Верифицированных интерфейсов объектов путем доказательства правильности передачи типов и количества данных в параметрах сообщений, заданных в языке IDL. Интерфейс состоит из операций обращения к объекту, который посылает данные другому объекту через сообщение.

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

Доказательство  правильности построения ОМ для некоторой  ПрО состоит в следующем:

 

• вводятся дополнительные и/или удаляются лишние атрибуты объекта и его интерфейсов в ОМ, доказывается правильность объекта ОМ после изменений спецификации интерфейсов и взаимодействий с другими объектами;
• доказывается правильность задания типов для атрибутов объекта, т.е. подтверждения того, что выбранный тип реализует операцию, а множество его значений определено на множестве состояний этого объекта;
• доказывается правильность спецификации объектов ОМ и параметров интерфейсов, которые передаются другим объектам. Этим заканчивается заключительное доказательство проверки правильности ОМ.

 

Верификация модели распределенного приложения - это спецификация процессов SDL (Spesification Description Language), задание модели проверки (model-checking) и индуктивных утверждений. В нем проверки состоит в редукции системы с бесконечным числом состояний к системе с конечным числом состояний, а также в доказательстве распределенных приложений с помощью индуктивных рассуждений и системы переходов конечного автомата.

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