ВПнМ, 01 лекция (от 08 февраля)
Материал из eSyr's wiki.
Верификация программ на моделях, Верификация моделей программ, Model checking.
В курсе матлогики, который нам очень понравился, на последней лекции рассматривали два подхода к верификации: верификация теорем и верификация моделей программ. Между двумя курсами есть различие: в курсе матлогики была внутренняя логика и математичкий формализм, этот же курс направлен на практическую сторону.
В качестве инструментального средства будем использовать программу Spin.
По курсу будет практикум, проходить он будет в 758 комнате.
План лекции
- Правильность программ
- Актуальность верификации
- Формальные методы
- Автоматизация
- История развития и области применения
- Обзор курса
- Практикум
Эта лекция вводная. Лектор расскажет, что такое правильность программ, почему её надо проверять строгими методами. Сделает небольшой обзор методов проверки правильности программ, расскажет, как развивалась эта область, и то, как будет устроен практикум и зачёт по этому курсу. Будет экзамен. Зачёт лектор отменил, допущены будут все.
Разработка программы
Ошибки появляются в ходе разработки программы. Существуют различные модели жизненного цикла, но можно выделить основные этапы:
- Анализ
- Проектирование, в ходе которого разрабатывается архитектура системы
- Реализация
- Темтированик
- Эксплуатация, в ходе которой внедряется система, исопльзуется
Ошибки могут появляться на всех этих этапах. В ходе анализа можно не так понять пользователя, в ходе разработки архитектуры, есть ошибки в ходе тестирования и эксплуатации.
Наибольшее количество ошибок вносится на этапах проектирования и реализации. Обнаруживаются на этапе тестирования, особенно сборочного. Выглядит всё неплохо, но цена ошибки резко возврастает в ходе эксплуатации.
Правильность программ
Что такое ошибка? Ошибка --- несоответствие требованиям. Если нет требований к программе, то нет неправильности. Программа не может быть ни правильной, ни неправильной в таком случае, она может быть забавной.
Ошибки бывают в формулировке требований и в их соблюдении.
Ошибки в формулировке: реализовано вроде всё правильно, а пользователь скажет, что здесь ошибка. Такие ошибки выявляются в ходе процесса, называемого валидация.
Все другие ошибки, которые есть, выявляются во время разработки программы. Процесс поиска этих ошибок --- процесс верификации: проверка, соответствует ли реализация спецификации. При этом считается, что спецификация правильная.
В ходе верификации/валидвции нужно найти ошибки, или доказать, что их нет.
Когда средство создаётся, средств на тестирование обычно нет. Но существуют другие системы, в которых ошибок не должно быть ни при каких обстоятельствах. Это системы с повышенными требованиями к надёжности. Это системы либо с большой ценой ошибки, либо приводящие к невосполнимым потерям.
Примеры:
- Ariana-5. Июнь 1996, взрыв ракеты спустя 40 секунд после старта. Ущерб --- 500 млн., стоимость разработки --- 7 млрд., причина ошибки: преобразования 64-bit float в 16-bit int
- Patriot: округление 24-bit fixed
- Sleipner A. Причина — ошибка округления при моделировании платформы.
Соответственно, для проверки правильности систем с повышенными требованиями к надёжности выборочное тестирование не подходит, и, как сказал Дейкстра, тестирование может выявить ошибки, но не показать, что их нет.
Тестирование направлено на выявление частых ошибок. Формальные методы направлены на поиск критических ошибок. Соотвтественно, редкие безвредные ошибки никого не интересуют.
Задача верификации программ в общем случае алгоритмически неразрешима. Таким образом, применение формальных методов, несмотря на общее мнение, что там что-то доказывается, что невозможно, там приводится обоснование, что их нет.
В абсолютном большинстве встречающиеся в природе системы таковы, что их ошибочность можно доказать, и это признак хорошего дизайна. По англицки это называется probably correct.
Формальные методы
ФМ --- использование матаппарата, реализованного в языках, методах и средствах спецификации и верификации программ.
- Методы формальной спецификации
- Верификация
- Доказательство теорем
- Верификация на моделях
Методы верификации
- Полное тестирование. Тестирование, в ходе которого при построении тестового набора приводится обоснование, что набор полный.
- Имитационное тестирование. Это то же тестирование, только оно помогает избежать в том случае, например, если система ещё не готова.
- Доказательство теорем
- Статический анализ
- Верификация на моделях
Тестирование
Грубо разделим эти методы на методы чёрного ящика, которые основываются на полном покрытии входных данных, и метод прозрачного ящика,который основывается на полном покрытии кода.
Плюсы:
- Проверяется та программа, которая будет использоваться
- Для проведения теста не требуется дополнительных инструментальных средств
- Удобная локализация ошибки. Средства тетстирования и отладки очень хорошо позволяют найти место в коде, где она находится
Минусы:
- Не всегда есть условия для тестирования системы
- Проблема с воспроизводимостью тестов. Ошибка должна быть воспроизводима для понимания и отладки. Если речь идёт про системы взаимодействия с реальным окружением или когда она связана с историей взаимодействия, то в этих случаях ошибка может быть невоспроизводима.
Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д.
Обоснование полноты тестового покрытия:
- ЧЯ: для последовательных программ сложно перебрать все входные данные
- ЧЯ: для параллельных дополнительно возникают цепочки взаимодействия и перестановки
- ЧЯ: для динамических структур, взаимодейсьвующих с окружением --- невозможно
- ПЯ: большой размер покрытия, растёт экспоненциально с размером
- Часто невозможно построение 100% покрытия.
- Полное покрытие не гарантирует отсутствие ошибков.
Пример: полное покрытие для ЧЯ:
- Поиск выигрышной стратегии в шашках --- 10^14 операций (?)
полное покрытие для прозрачного ящика:
- //пример с ифами
Для программы 1 нельзя построить полное покрытие
Для второй программы с двумя ошибками можно построить покрытие a, bbb, но оно не найдёт ни одну из них.
Итоги:
- Полный перебор входных данных --- невозможен
- Полнота покрытия кода не гарантирует правильности
!! Полнота вычислений
Реактивные программы
Эти программы работают в бесконечном цикле и взаимодействуют с окружением. Эти программы работают в терминах стимул/реакция. Здесь и возникает цепочка взаимодействия, которая резко увеличивает количество состояний системы, и обойти их тестированием не представляется возможным.
Реактивные программы это не пыльный ... на задворках программистких технологий, и ошбики там гораздо менее очевидны. Пример --- системы с разделением ресурсов.
Системы с разделением ресурсов
- Дорожный траффик. Пример с дедлоком на перекрёстке
- Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка.
- ОС. Пример с дедлоком
- ...
Параллельные системы
Новый источник ошибок --- совместная работа проверенных компонентов.
Обычно считается, что программы надо строить из небольших компонент. Потом их интегрируем и всё работает. Однако, возникают ошбки на другом уровне: в 1993 году аэробус садился на мокрую полосу, нужно было включить реверс, но он включился поздно, потому что для его включения нужно, чтобы крутились колёса,были выпущены шасси и было давление на колёса, что случилось не сразу.
Дополнительную сложность вносит одновременная работа.
Доказательство теорем
Есть система, свойства, есть аксиомы и правила вывода, и с помощью последних доказываются свойства.
Фото 3: проверить свойство, верно ли, что за a выполнится с? С помощью правил вывода мы можем показать, что правило выполняется.
К достоинствам относится тот факт, что можно доказывать для систем с бесконечным количеством состояний. Также даёт более глубокое понимание системы, даже более глубокое, чем нужно. Недостатки: меделнная работа, требуется помощь человека, неполнота аксиом в общем случае
Статический анализ
- Анализ текста программы без его выполнения. Можно сказать, что здесь обходим граф потока управления. В общем случае задача достижимости неразрешима, и в общем случае стат. анализ представляет компромисс между возм. и потребностями. Кроме того, удобные инженерные конструкции очень плохо поддаются статич. анализу.
Однако есть достаточно узкие области, где стат. анализ хорошо применим.
Расширяем множество значениий m неиниц. сост. Начальное сост. --- неиниц. И далее вычисляем отображение для каждой точки программы.
Видим, что перем. иниц. только при размере массива больше 0.
Достоинства стат. мод.: высокая скорость, ответу, если он дан, можно верить. Из минусов --- узкая обл. применения, а также ручная настройка при изм. проверяемых свойств.
Верификация программ на моделях
Можно построить модель с конеяч. кол. сост., сформулировать свойства, послед знач. предикатов и выполнить поиск по прост. сост., что дасто ответ на вопрос, выполняются свойства или нет. Доказывается, что либо свойства вып. на всех сост. модели, либо свойство не вып.
Что нам важно:
- программа может наход. в сост. открыта/закрыта
- Сост. меняются в двух местах
Итого 4 состояния.
Контрпример --- ошибка в процессе. Нашли ошибку.
Процесс вериф. сост. из 3 этапов:
- Моделирование. Строим адекватную корректную модель. Цель моделирования --- объяснить. У нас есть программа, есть инструментальное средство вериф. У него есть свой язык. Иногда это делается путём трансляции с языка напис. программы на вх. язык средства. Но при этом может получиться слишком сложная модель. Тогда необходима абстракция, которая упрощает можель. Модель при этом должна быть корректной и адекватной. Более детально это будет рассм. на след. лекциях. Коррект. моель корректно моделирует., а адекватная корректно экстраполирует св-ва на систему. Поскольку мы от чего-то абстрагируемся, оставляя то, что нужно, нужно знать, что нужно; модель без задачи не имеет смысла. Но обычно здесь формулируется класс свойств, например, корректна ли программа работает с разделяемыми ресурсами. тогда построим модель программы, которая работает с разд. рес., от остального абстрагируемся.
- Спецификация свойств. Это темпоральная логика плюс сс нккоторыми добавками, которые исп. Spin. Вопрос полноты свойств здесь не затрагивается. Это вопрос валидации и мы считаем, что свойства полны.
- Верификация. Мы передаём модель и св-ва в инстр. систему, нажимаем на кнопку проверить, и получаем контрпример. Дальше нужно понять, о чём контрпример говорит, анализ кп это прерогатива человека, котрый разбирается, что произошло: некорректная модель, модель не подходит для свойств, неправльная модель. Однако, если контрпример подтверждается, то мы нашли ошибку. Исправляем её и запускаем заново. Если модель конечная адекватна, то мы гарантированно получис ответ. Она позволяет выялвять редкие ошибки, которые обычно тестирование не выявляются.
Недостаток: работает только для конечных моделей. Бывают такие программы и св-ва, которые нельзя проверить с помощью конечной модели. Если кто-то захочет проверить самоприменимость, то никакая верификация не поможет.
Автоматизируемость
- Автоматизированное тестирование --- автомат. вып. тестов, это было давно. Автоматического тестирования нет.
- Доказательство теорем --- участие человека существенно
- Статич. анализ полностью автомат. в данной области и для данного св-ва
- Верификация - участие человека сводится к постр. модели и анализе контрпримеров. Проблема --- комбинаторный взрыв.
История развития
- Флойд, 1967. Ф. предложил использовать assertions, и выдвитнул гипотезу, что если у нас для некоторого ЯП описаны ass., то, с учётом того, как влияет оно на вып., можно доказать, что программа корректна
- Хоар ввёл триплеты (P | S | Q) и ввёл логич. вывод, и в первое время это делалось вручную.
- Первый автоматический прувер --- 1971
- Дейкстра, 1975 описал язык, который более удачно позволял доказывать корр. программ. Каждому операторы сопоставллялся guard, причём если было условие, то гарды выполнялись недетерменированно.
- Хоар, 1978 описал CSP --- взаимод. посл. процессы, это позв. доказывать корр. распред. программ
Развитие методов
- Пнуэли, 1977 --- темпоральная логика, LTL. Стало возм. описывать свойства подмножеством языка и выполнимость словами языка (?)
- Пнуэли, 1981 --- предложена логика ветвящегося времени, которая лучше подходит для тонких св-в пар. программ
- Клар, Эмерсон, 1981 --- предложен model checking, когда предст. программу в виде автомата с конеч. чслом сост., обходим дост. сост. и проверяем св-ва.
- Варди и Вольпер, 1986 -- анализ комформности в model checking, это снимает огр. на конеч. число сост.
В основном курсе будет уделять ся первому моделчекингу
- Хольцман, 1981. Построен верификатор Spin
Проблема комбинаторного взрыва
- Бриан, 1989. Двоичные решающие диаграммы (BDD) --- мы строим пространство сост., и склеиваем ветви согласно ряду правил
- МакМиллан, 1993. Верификатор SMV, исп. BDD
- Хольцман, Пелед, 1994 --- верификация паралл. систем.. Довольно часто бывает так, что порядок обмена не важен, тогда можно рассм. один из возможных --- редукция част. порядков
- 1995. Редукция част. порядков в Spin
после этого стало возм. применять верификаторы в промышленности.
Дальнейшее развитие
Было направлено на решение задачи комбинаторного взрыва
- Кларк, 1992 --- абстракцичя для уменьш. модели
- Эльсаиди, 1994 --- семант. минимиз
- Пелед, 1996 Бир, 1998 --- вериф. на лету, подгрузка по мере анализа и удаление просм. куска дерева из памяти
- Расси, 2000 - анализ достижимости с учётом специф. --- выбор эвристики на осн. св-в
- Эмерсон и Прасад, 1994 --- симметрия
Области применения вериф. на моделях
- Сетевые и криптограф. протоколы
- Протоколы работы кэш-памяти
- Инт. схемы
- Стандарты
- Встроенные системы
- Драйвера
- Вообще программы на С. Для Spic есть конвертер из C в его внутр. язык
Верификация программ на моделях
Календарь
| пт | пт | пт | пт | пт | |
Февраль
| 08 | 15 | 22 | 29 | |
Март
| 14 | 21 | 28 | ||
Апрель
| 04 | 11 | 18 |
Материалы по курсу
Список вопросов к экзамену | Примеры задач: 1 2 3 4 5 | Теормин
