Редактирование: ВПнМ, 01 лекция (от 08 февраля)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1: | Строка 1: | ||
- | '''Оригинальная презентация:''' http://savenkov.lvk.cs.msu.su/mc/lect1.ppt | ||
- | |||
Верификация программ на моделях, Верификация моделей программ, Model checking. | Верификация программ на моделях, Верификация моделей программ, Model checking. | ||
Строка 20: | Строка 18: | ||
Эта лекция вводная. Лектор расскажет, что такое правильность программ, почему её надо проверять строгими методами. Сделает небольшой обзор методов проверки правильности программ, расскажет, как развивалась эта область, и то, как будет устроен практикум и зачёт по этому курсу. Будет экзамен. Зачёт лектор отменил, допущены будут все. | Эта лекция вводная. Лектор расскажет, что такое правильность программ, почему её надо проверять строгими методами. Сделает небольшой обзор методов проверки правильности программ, расскажет, как развивалась эта область, и то, как будет устроен практикум и зачёт по этому курсу. Будет экзамен. Зачёт лектор отменил, допущены будут все. | ||
- | == Разработка программы == | + | ==Разработка программы == |
Ошибки появляются в ходе разработки программы. Существуют различные модели жизненного цикла, но можно выделить основные этапы: | Ошибки появляются в ходе разработки программы. Существуют различные модели жизненного цикла, но можно выделить основные этапы: | ||
Строка 26: | Строка 24: | ||
* Проектирование, в ходе которого разрабатывается архитектура системы | * Проектирование, в ходе которого разрабатывается архитектура системы | ||
* Реализация | * Реализация | ||
- | * | + | * Темтированик |
- | * Эксплуатация, в ходе которой внедряется система, | + | * Эксплуатация, в ходе которой внедряется система, исопльзуется |
Ошибки могут появляться на всех этих этапах. В ходе анализа можно не так понять пользователя, в ходе разработки архитектуры, есть ошибки в ходе тестирования и эксплуатации. | Ошибки могут появляться на всех этих этапах. В ходе анализа можно не так понять пользователя, в ходе разработки архитектуры, есть ошибки в ходе тестирования и эксплуатации. | ||
- | Наибольшее количество ошибок вносится на этапах проектирования и реализации. Обнаруживаются на этапе тестирования, особенно сборочного. Выглядит всё неплохо, но цена ошибки резко | + | Наибольшее количество ошибок вносится на этапах проектирования и реализации. Обнаруживаются на этапе тестирования, особенно сборочного. Выглядит всё неплохо, но цена ошибки резко возврастает в ходе эксплуатации. |
== Правильность программ == | == Правильность программ == | ||
Строка 43: | Строка 41: | ||
Все другие ошибки, которые есть, выявляются во время разработки программы. Процесс поиска этих ошибок --- процесс верификации: проверка, соответствует ли реализация спецификации. При этом считается, что спецификация правильная. | Все другие ошибки, которые есть, выявляются во время разработки программы. Процесс поиска этих ошибок --- процесс верификации: проверка, соответствует ли реализация спецификации. При этом считается, что спецификация правильная. | ||
- | В ходе верификации/ | + | В ходе верификации/валидвции нужно найти ошибки, или доказать, что их нет. |
Когда средство создаётся, средств на тестирование обычно нет. Но существуют другие системы, в которых ошибок не должно быть ни при каких обстоятельствах. Это системы с повышенными требованиями к надёжности. Это системы либо с большой ценой ошибки, либо приводящие к невосполнимым потерям. | Когда средство создаётся, средств на тестирование обычно нет. Но существуют другие системы, в которых ошибок не должно быть ни при каких обстоятельствах. Это системы с повышенными требованиями к надёжности. Это системы либо с большой ценой ошибки, либо приводящие к невосполнимым потерям. | ||
Строка 58: | Строка 56: | ||
Задача верификации программ в общем случае алгоритмически неразрешима. Таким образом, применение формальных методов, несмотря на общее мнение, что там что-то доказывается, что невозможно, там приводится обоснование, что их нет. | Задача верификации программ в общем случае алгоритмически неразрешима. Таким образом, применение формальных методов, несмотря на общее мнение, что там что-то доказывается, что невозможно, там приводится обоснование, что их нет. | ||
- | В абсолютном большинстве встречающиеся в природе системы таковы, что их ошибочность можно доказать, и это признак хорошего дизайна. По | + | В абсолютном большинстве встречающиеся в природе системы таковы, что их ошибочность можно доказать, и это признак хорошего дизайна. По англицки это называется probably correct. |
== Формальные методы == | == Формальные методы == | ||
- | ФМ | + | ФМ --- использование матаппарата, реализованного в языках, методах и средствах спецификации и верификации программ. |
* Методы формальной спецификации | * Методы формальной спецификации | ||
Строка 70: | Строка 68: | ||
== Методы верификации == | == Методы верификации == | ||
- | * Полное тестирование. Тестирование, в ходе которого при | + | * Полное тестирование. Тестирование, в ходе которого при постр. тестового набора приводится обосн., что набор оплный. |
- | * Имитационное тестирование. Это то же тестирование, только оно помогает избежать в том случае, например, если | + | * Имитационное тестирование. Это то же тестирование, только оно помогает избежать в том случае, например, если симстема ещё не готова. |
- | * | + | * Док. теорем |
* Статический анализ | * Статический анализ | ||
* Верификация на моделях | * Верификация на моделях | ||
=== Тестирование === | === Тестирование === | ||
- | Грубо разделим эти методы на | + | Грубо разделим эти методы на метод чёрного ящика, которые основываются на полном покрытии входных данных, метод прозрачного ящика основывается на полном покрытии кода. |
Плюсы: | Плюсы: | ||
* Проверяется та программа, которая будет использоваться | * Проверяется та программа, которая будет использоваться | ||
- | * Для проведения теста не требуется дополнительных | + | * Для проведения теста не требуется дополнительных интсрументальных средств |
- | * Удобная локализация ошибки. Средства | + | * Удобная локализация ошибки. Средства тетстирования и отладки очень хорошо позволяют найти место в коде, где она находится |
Минусы: | Минусы: | ||
* Не всегда есть условия для тестирования системы | * Не всегда есть условия для тестирования системы | ||
- | * Проблема с воспроизводимостью тестов. Ошибка должна быть воспроизводима для понимания и отладки. Если речь идёт про системы | + | * Проблема с воспроизводимостью тестов. Ошибка должна быть воспроизводима для понимания и отладки. Если речь идёт про системы взаимод. с реальным окружением, в этом случае она может быть невоспроизводима, или когда она связана с историей взаимодействия |
Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д. | Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д. | ||
- | Обоснование | + | Обоснование оплноты тстового покрытия: |
* ЧЯ: для последовательных программ сложно перебрать все входные данные | * ЧЯ: для последовательных программ сложно перебрать все входные данные | ||
- | * ЧЯ: для параллельных дополнительно возникают цепочки | + | * ЧЯ: для параллельных дополнительно возникают цепочки взаимод. и перестановки |
- | * ЧЯ: для динамических структур, | + | * ЧЯ: для динамических структур, взаимод. с окружением --- невозможно |
- | * ПЯ: большой размер покрытия, растёт | + | * ПЯ: большой размер покрытия, растёт жкспоненциально с размером |
- | * Часто невозможно | + | * Часто невозможно постр. 100% покрытик |
- | * Полное покрытие не гарантирует | + | * Полное покрытие не гарантирует отсут. ошибков. |
Пример: полное покрытие для ЧЯ: | Пример: полное покрытие для ЧЯ: | ||
- | * Поиск выигрышной стратегии в шашках | + | * Поиск выигрышной стратегии в шашках --- 10^14 операций (?) |
- | + | полное покрытие для прозрачного ящика: | |
- | + | * //пример с ифами | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | Для программы 1 нельзя построить полное покрытие | |
- | + | ||
- | + | Для второй программы с двумя ошибками можно построить покрытие a, bbb, но оно не найдёт ни одну из них. | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
Итоги: | Итоги: | ||
- | * Полный перебор | + | * Полный перебор вх. данных --- невозможен |
- | * | + | * Полноа покрытия кода не гарантирует правильности |
- | + | !! Полнота вычислений | |
==== Реактивные программы ==== | ==== Реактивные программы ==== | ||
- | + | Эти программы работают в бесконечном цикле и взаимод. с окружении. Эти программы работают в терминах стимул/реакция. Здесь и возникает цепочка взаимод, которая резко увеличивает сост. системы, и обойти их тестированием не предст. возможным. | |
- | + | Реакт. программы это не пыльный ... на задворках программистких технологий, и ошбики там гораздо менее очевидны. Пример --- системы с разделением ресурсов. | |
- | + | == Системы с разделением ресурсов == | |
- | + | * Дорожный траффик. Пример с дедлоком на перекрёстке | |
- | + | ||
- | * Дорожный | + | |
* Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка. | * Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка. | ||
* ОС. Пример с дедлоком | * ОС. Пример с дедлоком | ||
* ... | * ... | ||
- | + | == Параллельные системы == | |
Новый источник ошибок --- совместная работа проверенных компонентов. | Новый источник ошибок --- совместная работа проверенных компонентов. | ||
- | Обычно считается, что программы надо строить из небольших компонент. Потом их интегрируем и всё работает. Однако, возникают ошбки на другом уровне: в 1993 году аэробус садился на мокрую полосу, нужно было включить реверс, но он включился поздно, потому что для его включения нужно, чтобы крутились колёса, | + | Обычно считается, что программы надо строить из небольших компонент. Потом их интегрируем и всё работает. Однако, возникают ошбки на другом уровне: в 1993 году аэробус садился на мокрую полосу, нужно было включить реверс, но он включился поздно, потому что для его включения нужно, чтобы крутились колёса, выпущены шасси и есть давление на колёса, что случилось не сразу. |
Дополнительную сложность вносит одновременная работа. | Дополнительную сложность вносит одновременная работа. | ||
- | + | == Доказательство теорем == | |
- | Есть система, свойства, есть аксиомы | + | Есть система, свойства, есть аксиомы иправила вывода, и с помощью последних доказываются свойства. |
- | + | ||
- | + | ||
- | + | Фото 3: проверить свойство, верно ли, что за a выполнится с? С помощью правил вывода мы можем показать, что правило выполняется. | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | С помощью | + | |
- | К | + | К достоинствам относится тот факт, что можно доказывать для систем с беск. кол. сост. Также даёт более глубокое понимание системы, даже более глубокое, чем нужно. |
+ | Недостатки: меделнная работа, требуется помощь человека, неполнота аксиом в общем случае | ||
- | + | == Статический анализ == | |
+ | * Анализ текста программы без его выполнения. Можно сказать, что здесь обходим граф потока управления. В общем случае задача достижимости неразрешима, и в общем случае стат. анализ представляет компромисс между возм. и потребностями. Кроме того, удобные инженерные конструкции очень плохо поддаются статич. анализу. | ||
- | + | Однако есть достаточно узкие области, где стат. анализ хорошо применим. | |
- | + | ||
- | + | Расширяем множество значениий m неиниц. сост. | |
- | + | Начальное сост. --- неиниц. И далее вычисляем отображение для каждой точки программы. | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | Начальное | + | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | Видим, что | + | Видим, что перем. иниц. только при размере массива больше 0. |
- | + | Достоинства стат. мод.: высокая скорость, ответу, если он дан, можно верить. Из минусов --- узкая обл. применения, а также ручная настройка при изм. проверяемых свойств. | |
- | + | == Верификация программ на моделях == | |
[[Изображение:Savenkov 1.jpg|thumb|240px|left]] | [[Изображение:Savenkov 1.jpg|thumb|240px|left]] | ||
- | Можно построить модель с | + | Можно построить модель с конеяч. кол. сост., сформулировать свойства, послед знач. предикатов и выполнить поиск по прост. сост., что дасто ответ на вопрос, выполняются свойства или нет. Доказывается, что либо свойства вып. на всех сост. модели, либо свойство не вып. |
Что нам важно: | Что нам важно: | ||
- | * программа может | + | * программа может наход. в сост. открыта/закрыта |
- | * | + | * Сост. меняются в двух местах |
Итого 4 состояния. | Итого 4 состояния. | ||
- | Контрпример | + | Контрпример --- ошибка в процессе. Нашли ошибку. |
- | Процесс | + | Процесс вериф. сост. из 3 этапов: |
- | * Моделирование. Строим адекватную корректную модель. Цель моделирования --- объяснить. У нас есть программа, есть инструментальное средство | + | * Моделирование. Строим адекватную корректную модель. Цель моделирования --- объяснить. У нас есть программа, есть инструментальное средство вериф. У него есть свой язык. Иногда это делается путём трансляции с языка напис. программы на вх. язык средства. Но при этом может получиться слишком сложная модель. Тогда необходима абстракция, которая упрощает можель. Модель при этом должна быть корректной и адекватной. Более детально это будет рассм. на след. лекциях. Коррект. моель корректно моделирует., а адекватная корректно экстраполирует св-ва на систему. Поскольку мы от чего-то абстрагируемся, оставляя то, что нужно, нужно знать, что нужно; модель без задачи не имеет смысла. Но обычно здесь формулируется класс свойств, например, корректна ли программа работает с разделяемыми ресурсами. тогда построим модель программы, которая работает с разд. рес., от остального абстрагируемся. |
- | * Спецификация свойств. Это темпоральная логика плюс | + | * Спецификация свойств. Это темпоральная логика плюс сс нккоторыми добавками, которые исп. Spin. Вопрос полноты свойств здесь не затрагивается. Это вопрос валидации и мы считаем, что свойства полны. |
- | * Верификация. Мы передаём модель и | + | * Верификация. Мы передаём модель и св-ва в инстр. систему, нажимаем на кнопку проверить, и получаем контрпример. Дальше нужно понять, о чём контрпример говорит, анализ кп это прерогатива человека, котрый разбирается, что произошло: некорректная модель, модель не подходит для свойств, неправльная модель. Однако, если контрпример подтверждается, то мы нашли ошибку. Исправляем её и запускаем заново. Если модель конечная адекватна, то мы гарантированно получис ответ. Она позволяет выялвять редкие ошибки, которые обычно тестирование не выявляются. |
- | Недостаток: работает только для конечных моделей. Бывают такие программы и | + | Недостаток: работает только для конечных моделей. Бывают такие программы и св-ва, которые нельзя проверить с помощью конечной модели. Если кто-то захочет проверить самоприменимость, то никакая верификация не поможет. |
== Автоматизируемость == | == Автоматизируемость == | ||
- | * Автоматизированное тестирование | + | * Автоматизированное тестирование --- автомат. вып. тестов, это было давно. Автоматического тестирования нет. |
- | * Доказательство теорем | + | * Доказательство теорем --- участие человека существенно |
- | * | + | * Статич. анализ полностью автомат. в данной области и для данного св-ва |
- | * Верификация - участие человека сводится к | + | * Верификация - участие человека сводится к постр. модели и анализе контрпримеров. Проблема --- комбинаторный взрыв. |
== История развития == | == История развития == | ||
- | * Флойд, 1967. Ф. предложил использовать assertions, и | + | * Флойд, 1967. Ф. предложил использовать assertions, и выдвитнул гипотезу, что если у нас для некоторого ЯП описаны ass., то, с учётом того, как влияет оно на вып., можно доказать, что программа корректна |
- | * Хоар ввёл триплеты (P | S | Q) и ввёл | + | * Хоар ввёл триплеты (P | S | Q) и ввёл логич. вывод, и в первое время это делалось вручную. |
* Первый автоматический прувер --- 1971 | * Первый автоматический прувер --- 1971 | ||
- | * Дейкстра, 1975 описал язык, который более удачно позволял доказывать | + | * Дейкстра, 1975 описал язык, который более удачно позволял доказывать корр. программ. Каждому операторы сопоставллялся guard, причём если было условие, то гарды выполнялись недетерменированно. |
- | * Хоар, 1978 описал CSP --- | + | * Хоар, 1978 описал CSP --- взаимод. посл. процессы, это позв. доказывать корр. распред. программ |
=== Развитие методов === | === Развитие методов === | ||
- | * Пнуэли, 1977 --- темпоральная логика, LTL. Стало | + | * Пнуэли, 1977 --- темпоральная логика, LTL. Стало возм. описывать свойства подмножеством языка и выполнимость словами языка (?) |
- | * Пнуэли, 1981 --- предложена логика ветвящегося времени, которая лучше подходит для тонких | + | * Пнуэли, 1981 --- предложена логика ветвящегося времени, которая лучше подходит для тонких св-в пар. программ |
- | * Клар, Эмерсон, 1981 --- предложен model checking, когда | + | * Клар, Эмерсон, 1981 --- предложен model checking, когда предст. программу в виде автомата с конеч. чслом сост., обходим дост. сост. и проверяем св-ва. |
- | * Варди и Вольпер, 1986 -- анализ | + | * Варди и Вольпер, 1986 -- анализ комформности в model checking, это снимает огр. на конеч. число сост. |
В основном курсе будет уделять ся первому моделчекингу | В основном курсе будет уделять ся первому моделчекингу | ||
- | * Хольцман, | + | * Хольцман, 1981. Построен верификатор Spin |
=== Проблема комбинаторного взрыва === | === Проблема комбинаторного взрыва === | ||
- | * Бриан, 1989. Двоичные решающие диаграммы (BDD) --- мы строим пространство | + | * Бриан, 1989. Двоичные решающие диаграммы (BDD) --- мы строим пространство сост., и склеиваем ветви согласно ряду правил |
- | * МакМиллан, 1993. Верификатор SMV, | + | * МакМиллан, 1993. Верификатор SMV, исп. BDD |
- | * Хольцман, Пелед, 1994 --- верификация | + | * Хольцман, Пелед, 1994 --- верификация паралл. систем.. Довольно часто бывает так, что порядок обмена не важен, тогда можно рассм. один из возможных --- редукция част. порядков |
* 1995. Редукция част. порядков в Spin | * 1995. Редукция част. порядков в Spin | ||
- | + | после этого стало возм. применять верификаторы в промышленности. | |
=== Дальнейшее развитие === | === Дальнейшее развитие === | ||
Было направлено на решение задачи комбинаторного взрыва | Было направлено на решение задачи комбинаторного взрыва | ||
- | * Кларк, 1992 --- | + | * Кларк, 1992 --- абстракцичя для уменьш. модели |
- | * Эльсаиди, 1994 --- | + | * Эльсаиди, 1994 --- семант. минимиз |
- | * Пелед, 1996 Бир, 1998 --- | + | * Пелед, 1996 Бир, 1998 --- вериф. на лету, подгрузка по мере анализа и удаление просм. куска дерева из памяти |
- | * Расси, 2000 - анализ достижимости с учётом | + | * Расси, 2000 - анализ достижимости с учётом специф. --- выбор эвристики на осн. св-в |
* Эмерсон и Прасад, 1994 --- симметрия | * Эмерсон и Прасад, 1994 --- симметрия | ||
- | == Области применения | + | == Области применения вериф. на моделях == |
- | * Сетевые и | + | * Сетевые и криптограф. протоколы |
* Протоколы работы кэш-памяти | * Протоколы работы кэш-памяти | ||
- | * | + | * Инт. схемы |
* Стандарты | * Стандарты | ||
* Встроенные системы | * Встроенные системы | ||
* Драйвера | * Драйвера | ||
- | * Вообще программы на С. Для | + | * Вообще программы на С. Для Spic есть конвертер из C в его внутр. язык |
{{ВПнМ}} | {{ВПнМ}} | ||
{{Lection-stub}} | {{Lection-stub}} |