Верификация программ на моделях Константин Савенков (лектор) Игорь Коннов

План лекции Правильность программ Актуальность верификации Формальные методы Автоматизация История развития и области применения Обзор курса Практикум

Разработка программы Анализ Проектиро- вание Реали- зация Тестирование Эксплуа- тация UnitSystem Внесённые ошибки Обнаруженные ошибки Цена ошибки

Правильность программ Нет требований – нет правильности Ошибка – несоответствие требованиям Ошибки: –в формулировке требований, building the wrong system, –в соблюдении требований, building the system wrong.

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

Цена ошибки Системы с повышенными требованиями к надёжности (Safety- critical) Ошибки приводят к: –Гибели или травмам людей, –Крупным финансовым потерям –Ущербу окружающей среде –Итд.

Цена ошибки: Ariana-5 Июнь 1996 года, взрыв ракеты спустя 40 сек. после старта, Ущерб – $500млн (разработка – $7 млрд.), Причина – 64bit float -> 16bit int.

Цена ошибки: Patriot Февраль 1991 года, Patriot промахнулся мимо ракеты Scud, Ущерб – 28 убитых, >100 раненых, Причина – ошибка округления из-за 24bit fixed, Scud успел пролететь 500м.

Цена ошибки: Sleipner A август 1991 года, Северное море, платформа Sleipner A затонула после разрушения основания, Ущерб – $700 млн, землетрясение силой 3 балла, Причина – ошибка округления при моделировании платформы.

Выборочное тестирование «Тестирование может показать присутствие ошибок, но не может показать их отсутствия» (с) Дейкстра. безвредные критические Выявление ошибок частыередкие тести- рова ние формальные методы не важно

Reminder ВЕРИФИКАЦИЯ ПРОГРАММЫ В ОБЩЕМ СЛУЧАЕ АЛГОРИТМИЧЕСКИ НЕРАЗРЕШИМА

Формальные методы Методы формальной спецификации Методы формальной верификации: –Доказательство теорем –Верификация на моделях –Кое-что ещё «Использование математического аппарата, реализованного в языках, методах и средствах спецификации и верификации программ»

Методы верификации «Полное» тестирование Имитационное моделирование Доказательство теорем Статический анализ Верификация на моделях

Тестирование Обоснование полноты тестового покрытия, Метод «чёрного ящика» (ЧЯ) -- полное покрытие входных данных, Метод «прозрачного ящика» (ПЯ) -- полное покрытие кода программы.

Тестирование: плюсы Проверяется та программа, которая будет использоваться, Не требуется (знания) дополнительных инструментальных средств, Удобная локализация ошибки.

Тестирование: минусы Не всегда есть условия для тестирования системы, Проблема с воспроизводимостью тестов. частичное решение – имитационное моделирование

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

Полное покрытие для черного ящика Поиск выигрышной стратегии в шашках: –10 14 тестов, –18 лет, –постоянно работало от 50 до 200 десктопов.

Полное покрытие для прозрачного ящика if (B1) { S1; } if (B1) { S1; } if (B2) { S2; } - Два теста - Четыре теста …exp…

Полное покрытие для прозрачного ящика int x = 1; if (x == 1) { std::cout

Полное тестовое покрытие – не панацея int strlen(const char* p) { int len = 0; do { ++len; } while (*p++); return len; } «а», «bbb» -- полное покрытие кода, ошибка не найдена

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

Реактивные программы Традиционные программы: –Завершаются, –Описание «вход/выход», –Число состояний зависит от входных данных и переменных; Реактивные программы: –Работают в бесконечном цикле, –Взаимодействуют с окружением, –Описание «стимул/реакция», –(Не обязательно параллельные), –Дополнительный источник сложности.

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

Системы с разделением ресурсов Примеры: Дорожный траффик, Телефонные сети, Операционные системы, …

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

Доказательство теорем Система и свойства – формулы Набор аксиом и правил вывода Строится доказательство свойства- теоремы Качественный анализ системы

Доказательство теорем Система: Свойство: Правила вывода:

Доказательство теорем Достоинства: –работа с бесконечными пр-вами состояний, –даёт более глубокое понимание системы. Недостатки: –медленная скорость работы, –может потребоваться помощь человека (построение инвариантов циклов), –В общем случае нельзя построить полную систему аксиом и правил выводов.

Статический анализ Более грубый и прагматичный подход, Анализ исходного текста программы без её выполнения, В общем случае задача неразрешима, Поиск компромисса между потребностями и возможностями.

Статический анализ: пример Проверка инициализированности переменной: int min(int* arr, int n) { int m; if (n > 0) { m = arr[0]; } int i = 0; while (i < n) { if (m > arr[i]) { m = arr[i]; } i++; } return m; } dom(m) = Int + { ω } NI = { ω } I = Int v: Expr -> {NI, I}

Статический анализ: пример Проверка инициализированности переменной: int min(int* arr, int n) { int m; if (n > 0) { m = arr[0]; } (!) int i = 0; while (i { if (m > arr[i]) { m = arr[i]; } i++; } return m; } dom(m) = Int + { ω } NI = { ω } I = Int v: Expr -> {NI, I}

Статический анализ Достоинства –Высокая скорость работы, –Если ответ дан, ему можно верить. Недостатки –Узкая область применения (оптимизация в компиляторах, анализ похожести кода, анализ безопасности итп.), –Ручная настройка при изменении проверяемых свойств

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

Верификация программ на моделях: пример Всегда ли функция закрывает открытый файл ? int count_lines(const char* filename) { int c, count = 0; FILE* f = fopen(filename, "r"); if (f != NULL) { c = fgetc(f); while (c != EOF) { if (c == '\n') { ++count; } c = fgetc(f); } if (ferror(f)) { return -1; } fclose(f); return count; } else { return -1; }

Верификация программ на моделях: пример Модель функции count_lines: entryopenedclosed exit fopenfclosereturn f = NULL ferror(f) = 1

Процесс верификации программ на моделях Моделирование –Построить адекватную и корректную модель, –Избежать «лишних» состояний; Спецификация свойств –Темпоральная логика, –Полнота свойств; Верификация –Построение контрпримера, –Анализ контрпримера.

Верификация программ на моделях Достоинства –Хорошо автоматизируем, –Если модель конечна, корректна и адекватна проверяемому свойству, то даётся точный ответ, –Выявляет редкие ошибки. Недостатки –Работает только для конечных моделей.

Автоматизируемость Тестирование: автоматическое и автоматизированное, Доказательство теорем: существенное участие человека, Статический анализ: полностью автоматический для заданной области и свойства, Верификация на моделях: участие человека при построении модели и при анализе контрпримеров, «Комбинаторный взрыв».

История развития: фундамент Флойд, 1967 – assertions, гипотеза о доказуемости корректности программы, Хоар, 1969 – пред- и пост-условия, триплеты Хоара (P | S | Q), логический вывод, Бойер, Мур, 1971 – первый автоматический прувер, Дейкстра, 1975 – Guarded Command Languages, Хоар, 1978 – взаимодействующие последовательные процессы (CSP).

История развития: развитие методов Пнуэли, 1977 – темпоральная логика LTL, Пнуэли, 1981 – логика ветвящегося времени (CTL), Кларк, Эмерсон, 1981 и Квили, Сифакис, 1982 – model checking (обход достижимых состояний), Варди и Вольпер, 1986 – новая техника model checking (анализ конформности), Хольцман, 1981 – верификатор SPIN.

История развития: проблема «комбинаторного взрыва» Бриан, 1989 – Двоичные решающие диаграммы (BDD), МакМиллан, 1993 – верификатор SMV (символьная верификация, BDD), Хольцман, Пелед, 1994 – редукция частичных порядков, 1995 – редукция частичных порядков в SPIN.

История развития: дальнейшее развитие Кларк, 1992 – абстракция для уменьшения числа состояний модели, Эльсаиди, 1994 – семантическая минимизация, Пелед, 1996, Бир, 1998 – верификация модели «на лету», Равви, 2000 – анализ достижимости с учётом спецификации, Эмерсон, Прасад, симметрия

Рост мощности model checking 1992 год – 1020 состояний, 1994 год – состояний, 1998 год(?) – состояний

Области применения верификации на моделях Сетевые и криптографические протоколы, Протоколы работы кэш-памяти, Интегральные схемы, Стандарты (напр. FutureBus+), Встроенные системы, Драйвера, Вообще программы на C.

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

Литература Кларк, Грумберг, Пелед. Верификация моделей программ: Model checking, МЦНМО, Holzmann. The Spin Model Checker: Primer and Reference Manual, Addison Wesley, Сайт Spin:

Практикум и зачёт курса Ауд. 758, Linux, SPIN; Задачи – по мере прохождения курса; Экзамен, нерешённые задачи – на экзамене; Подписаться: Информация и задачи – по почте.

Спасибо за внимание!