МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ

РОССИЙСКОЙ ФЕДЕРАЦИИ

Ярославский государственный университет им. П.Г. Демидова

Факультет информатики и вычислительной техники

УТВЕРЖДАЮ

Проректор по развитию образования

_Е.В. Сапир "_"2012 г.

Рабочая программа дисциплины послевузовского профессионального образования (аспирантура) Верификация программного обеспечения по специальности научных работников 05.13.11 Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей Ярославль 1. Цели освоения дисциплины Целями освоения дисциплины «Верификация программного обеспечения» в соответствии с общими целями основной профессиональной образовательной программы послевузовского профессионального образования (аспирантура) (далее ОПП– образовательная программа послевузовского профессионального образования) являются:

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

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

Дисциплина «Верификация программного обеспечения» необходима для решения задач построения корректных программ, анализа корректности и исследования различных свойств программ и их моделей.

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

3. Требования к результатам освоения содержания дисциплины В результате освоения дисциплины обучающийся должен:

Знать:

1) способы моделирования программ;

2) способы спецификации и анализа свойств программ;

3) способы дедуктивного доказательства корректности программ;

4) стратегию спецификации и доказательства корректности программ, написанных на процедурном языке высокого уровня;

5) методы автоматической проверки корректности программной модели.

Уметь:

1) проводить спецификацию программ на языке предикатов;

2) применять метод доказательства теорем для доказательства корректности программ, написанных на языках высокого уровня;

3) строить программные модели и проводить спецификацию и верификацию программных свойств на языке темпоральной логики;

4) строить модели систем реального времени с помощью формализма временных автоматов и проводить спецификацию свойств таких систем на языках временных темпоральных логик.

Владеть:

1) формальными методами моделирования и спецификации программ;

2) формальными методами анализа корректности программ (алгоритмов):

дедуктивным анализом (метод доказательства теорем) и методом проверки модели (model checking).

4. Структура и содержание дисциплины «Верификация программного обеспечения»

Общая трудоемкость дисциплины составляет 3 зачетные единицы, 108 часов.

Курс № Раздел Виды учебной работы, Формы текущего Неделя примере «простого» языка программирования.

Спецификация программ с помощью пред- и постусловий.

Доказательство корректности программ относительно спецификации, инвариантов и ограничивающей функции.

Построение инвариантов и ограничивающих функций.

систем.Асинхронные и синхронные процессы.

Взаимодействие процессов.

Структура Крипке. Метод проверки модели.

Верификация моделей и теория автоматов. Автоматы над бесконечными словами.

Структура Крипке как автомат Бюхи. Темпоральная логика линейного времени LTL.

Формула LTL как обобщенный автомат Бюхи. Редукция автомата Бюхи для формулы LTL.

Пересечение языков структуры Крипке и автомата Бюхи.

Проверка пустоты автомата Бюхи.

Проверка модели «на лету».

CTL. Темпоральная логика CTL.

Верификация моделей для CTL.

Верификация моделей и неподвижные точки. Символьная верификация моделей для CTL.

Двоичные диаграммы решений.

Диаграммы ROBDD. Построение и манипуляция ROBDD.

4 Теория временных автоматов. 1 10-12 2/1 34/ Индивидуальное задание спецификация и верификация систем реального времени с помощью временных автоматов 5. Образовательные технологии В основу образовательной технологии по дисциплине «Верификация программного обеспечения» помимо традиционных форм занятий в виде лекций положена также форма, состоящая в выполнении обучающимся индивидуальных заданий по темам дисциплины.

Имеются четыре индивидуальных задания по дисциплине. Задания должны быть решены письменно или в электронном виде с последующей устной защитой. Первое задание закрывает тематику дедуктивного анализа корректности последовательных программ.

Представляет собой небольшую программу, написанную на «простом» языке высокого уровня, корректность которой необходимо доказать относительно спецификации, составляемой аспирантом по словесному описанию требований к программе. При безуспешных со стороны аспиранта попытках построения инварианта, ограничивающей функции и постусловия эти необходимые для выполнения задания компоненты могут быть предоставлены аспиранту. Выполнение второго, третьего и четвертого заданий предполагает моделирование (представление в виде структуры Крипке), спецификацию (запись свойств на языке темпоральной логики) и автоматическую верификацию некоторой параллельной и распределенной программы с помощью свободно распространяемых для учебных целей средств верификации SPIN, SMV и Uppaal.

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

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

Примеры индивидуальных заданий:

Докажите формально, что следующий алгоритм предназначен для записи в переменную z произведения чисел a и b при b 0 без использования операции умножения.

II. – III. Используя определения синтаксиса и семантики формул темпоральной логики LTL (или CTL) произведите спецификацию с последующей верификацией с помощью средства верификации SPIN и SMV указанных ниже свойств для системы асинхронных параллельных процессов со взаимным исключением, представленной на рис. 1.1. в пособии [4]:

1. «Взаимное исключение». Процессы никогда не окажутся в своих критических участках одновременно. Другими словами, система ни при каких обстоятельствах не попадет в состояние, в котором процессы Пр1 и Пр2 будут находиться в своих локальных состояниях с номерами 7.

2. «Отсутствие взаимной блокировки». Не существует ситуации, при которой ни процесс Пр1, ни процесс Пр2 не могут перейти в другое локальное состояние.

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

«Справедливость». Если оба процесса одновременно вышли из своих некритических участков, т. е. процессы Пр1 и Пр2 находятся в локальных состояниях с номерами 1, то в свой критический участок первым обязательно войдет тот процесс, приоритет которого в данным момент выше (приоритет определяется исходя из значения переменной trn).

5. «Отсутствие чередования». Если первый процесс только что посетил свой критический участок и хочет вновь в него войти, а второй процесс не выражает такого желания, то первому нет необходимости дожидаться, пока второй процесс проявит себя, войдет в критическую область, а затем покинет ее. Другими словами, посещения процессами своих критических участков не обязательно должны чередоваться. Если один из процессов навсегда остается в своем некритическом участке (например, закончил работу), то это не оказывает никакого влияния на возможность входа другого процесса в свой критический участок.

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