Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Расшифровка цветовых обозначений

Черное – взято из слайдов К.О. Савенкова 2010 года.

Красное – взято из книги Э.М. Кларка по верификации.

Синее – придумано мною или слито с esyr.org или рождено на форуме cmcspec.ru.

Делали: SLenik (полностью лекции 1-3, частично 4 и 5), <вставьте свою фамилию>

Лектор = Константин Олегович Савенков (слева)

Что-то краткое по курсу «Верификация моделей программ»

Этапы разработки программ:

• Анализ

• Проектирование

• Реализация

• Тестирование

• Эксплуатация

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

Задача верификации в общем случае алгоритмически неразрешима!

Методы верификации

Автоматизируемость методов верификации

• Тестирование: автоматическое и автоматизированное

• Доказательство теорем: существенное участие человека

• Статический анализ: полностью автоматический для заданной области и свойства

• Верификация на моделях: участие человека при построении модели и при анализе контрпримеров

Области применения верификации на моделях

• Сетевые и криптографические протоколы

• Протоколы работы кэш-памяти

• Интегральные схемы

• Стандарты

• Встроенные системы

• Драйвера

• Вообще программы на С

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

Моделирование программ

Модель – упрощённое описание реальности, выполненное с определенной целью.

• с каждым объектом может быть связано несколько моделей

• каждая модель отражает свой аспект реальности

Аспекты модели

• Простота – модель должна быть проще, чем реальность

• Корректность – не расходиться с реальностью

• Адекватность – соответствовать решаемой задаче

Построение модели

1. Формализация требований (постановка задачи моделирования)

2. Выбор языка моделирования

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

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

Состояние программы – совокупностью значений переменных программы и счетчиков управления последовательных процессов.

Состояние называется

Состояние называется потенциальным, если соответствующее состояние допустимо в рамках модели программы.

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

В общем случае задача определения достижимости состояния алгоритмически неразрешима.

Степень детализации (гранулярность) переходов

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

Для этого избегаем двух крайностей:

• Не определяем переходы «чрезмерно крупно» (модель программы может не включать некоторые наблюдаемые состояния – при верификации ошибки могут быть пропущены).

• Не описываем программу «излишне подробно» (могут образовываться новые состояния, которых в реальной программе никогда не будут достигнуты – при верификации могут обнаружиться призрачные ошибки, которые никогда не случаются на практике)

Формальное описание этапов верификации

В ходе верификации применяются различные представления программы

Размеченная система переходов (LTS)

где:

• – множество состояний [конечное или счетное]

• – множество действий (где – невидимое действие) [конечное]

• – тотальное отношение переходов. Тотальность означает, что для каждого состояния должно существовать такое состояние , что имеет место (или что из каждого состояния ведет какое-то действие)

• – множество начальных состояний

• – множество атомарных высказываний (некоторый набор свойств)

• – функция разметки (помечает каждое состояние множеством атомарных высказываний, истинных в данном состоянии).

Недетерминизм

В общем виде определения нет, только синоним – неопределенность.

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

Использование

• Моделирование параллельного выполнения процессов в режиме чередования (проверяем все возможные варианты параллельного выполнения с точностью до состояния)

• Моделирование прототипа системы (не ограничивает будущую реализацию заданным порядком выполнения операторов или конкретными входными данными)

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

Недетерминизм в LTS – проявляется в виде состояний, из которых можно перейти более, чем в одно состояния.

• Недетерминизм действий (может произойти одно из нескольких действий)

• Недетерминизм атомарных высказываний (наблюдатель не может отличить два состояния)

Строгое определение недетерминизма в LTS

Прямые потомки вершины s

• по действию a:

• по всем действиям:

Прямые предки вершины s

• по действию a:

• по всем действиям:

Размеченная система переходов детерминирована

• По действиям тогда и только тогда, когда: и

• По атомарным высказываниям тогда и только тогда, когда: и

Конечным путем системы переходов называется такая последовательность чередующихся состояний и действий, заканчивающихся состоянием: , что

Бесконечным путем системы переходов называется такая последовательность чередующихся состояний и действий: , что

Путь в системе переходов TS называется начальным, если

Путь в системе переходов TS называется максимальным, если он бесконечен.

Вычислением системы переходов TS называется начальный максимальный путь.

Состояние называется достижимым (из начального) в системе переходов TS, если существует начальный конечный путь, содержащий это состояние. – обозначение множества достижимых состояний в системе переходов TS.

Трасса для пути в системе переходов TS – последовательность множеств атомарных высказываний, записанных для каждого состояния пути в порядке следования состояний.

Свойство линейного времени определяет набор допустимых трасс

• Свойство выполнимо на трассе :

• Система переходов TS удовлетворяет свойству линейного времени : ,

Абстракция трасс

Представим трассу в форме интерпретации

• N – множество натуральных чисел

• – отношение порядка на N

• , и при этом

Рассмотрим две трассы = , .

является корректной абстракцией ( ), если:

1. (выбрали какие-то атомарные высказывания)

2. , т.ч. (придумали какую-то неубывающую натуральную функцию)

3. (и при помощи этой функции перенумеровали события, сохранив их порядок друг относительно друга)

Условие корректности модели

Пусть P – система, а – произвольное свойство линейного времени. Корректной моделью P называется такая модель M, для которой верно: если свойство выполняется на модели M, то оно выполняется и на системе P.

Это утверждение верно тогда и только тогда, когда для любой трассы исходной системы P в модели M найдется ее корректная абстракция.

Достаточное условие корректности модели

1. (отобрали какие-то действия)

2. (и какие-то атомарные высказывания)

3. (придумали какую-то неубывающую натуральную функцию)

4. (перенумеровали с ее помощью все отобранные состояния так, чтобы переходы, которые были между отобранными состояниями, сохранились)

5. (и попросили, чтобы функция разметки каждое из отобранных состояний размечала только отобранными атомарными высказываниями)

Адекватность модели

Модель называется адекватной, если

• (атомарные высказывания, в терминах которых задаются свойства, присутствуют в разметке модели)

• (из нарушения свойства на модели следует, что оно нарушается и на исходной системе)

Верификация программы при помощи модели

• Нужно знать, как система устроена и как она должна быть устроена.

• Соответственно, нужно две нотации:

  • Описание поведения (устройства системы)

  • Описание требований (свойств правильности)

• Выбранная нотация гарантирует разрешимость любого свойства любой модели.

Формальное представление программы

1. Граф, задающий структуру программы

2. Статическая семантика – набор ограничений, которым должна удовлетворять программа

3. Операционная семантика – понятие состояния программы, и изменение состояния в ходе работы программы.

– единый абстрактный домен данных (базовый тип для всех типов данных, тождественно равен типу int)

– множество переменных программы P.

Функция означивания переменной (возвращает тип переменной по ее имени)

– набор булевых условий над множеством .

Характеристики

Тип файла документ

Документы такого типа открываются такими программами, как Microsoft Office Word на компьютерах Windows, Apple Pages на компьютерах Mac, Open Office - бесплатная альтернатива на различных платформах, в том числе Linux. Наиболее простым и современным решением будут Google документы, так как открываются онлайн без скачивания прямо в браузере на любой платформе. Существуют российские качественные аналоги, например от Яндекса.

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

Файлы такого типа обычно разбиты на страницы, а текст может быть форматированным (жирный, курсив, выбор шрифта, таблицы и т.п.), а также в него можно добавлять изображения. Формат идеально подходит для рефератов, докладов и РПЗ курсовых проектов, которые необходимо распечатать. Кстати перед печатью также сохраняйте файл в PDF, так как принтер может начудить со шрифтами.

Список файлов лабораторной работы