Редактирование: ВПнМ, 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. |
== Формальные методы == | == Формальные методы == | ||
- | ФМ | + | ФМ --- использование матаппарата, реализованного в языках, методах и средствах спецификации и верификации программ. |
* Методы формальной спецификации | * Методы формальной спецификации | ||
Строка 82: | Строка 80: | ||
* Проверяется та программа, которая будет использоваться | * Проверяется та программа, которая будет использоваться | ||
* Для проведения теста не требуется дополнительных инструментальных средств | * Для проведения теста не требуется дополнительных инструментальных средств | ||
- | * Удобная локализация ошибки. Средства | + | * Удобная локализация ошибки. Средства тетстирования и отладки очень хорошо позволяют найти место в коде, где она находится |
Минусы: | Минусы: | ||
* Не всегда есть условия для тестирования системы | * Не всегда есть условия для тестирования системы | ||
- | * Проблема с воспроизводимостью тестов. Ошибка должна быть воспроизводима для понимания и отладки. Если речь идёт про системы взаимодействия с реальным окружением или когда она связана с историей взаимодействия, то в этих случаях ошибка может быть | + | * Проблема с воспроизводимостью тестов. Ошибка должна быть воспроизводима для понимания и отладки. Если речь идёт про системы взаимодействия с реальным окружением или когда она связана с историей взаимодействия, то в этих случаях ошибка может быть невоспроизводима. |
Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д. | Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д. | ||
Строка 92: | Строка 90: | ||
* ЧЯ: для последовательных программ сложно перебрать все входные данные | * ЧЯ: для последовательных программ сложно перебрать все входные данные | ||
* ЧЯ: для параллельных дополнительно возникают цепочки взаимодействия и перестановки | * ЧЯ: для параллельных дополнительно возникают цепочки взаимодействия и перестановки | ||
- | * ЧЯ: для динамических структур, | + | * ЧЯ: для динамических структур, взаимодейсьвующих с окружением --- невозможно |
* ПЯ: большой размер покрытия, растёт экспоненциально с размером | * ПЯ: большой размер покрытия, растёт экспоненциально с размером | ||
- | * Часто невозможно построение 100% покрытия | + | * Часто невозможно построение 100% покрытия. |
- | * Полное покрытие не гарантирует отсутствие | + | * Полное покрытие не гарантирует отсутствие ошибков. |
Пример: полное покрытие для ЧЯ: | Пример: полное покрытие для ЧЯ: | ||
- | * Поиск выигрышной стратегии в шашках | + | * Поиск выигрышной стратегии в шашках --- 10^14 операций (?) |
- | + | полное покрытие для прозрачного ящика: | |
- | + | * //пример с ифами | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | Для программы 1 нельзя построить полное покрытие | |
- | + | ||
- | + | Для второй программы с двумя ошибками можно построить покрытие a, bbb, но оно не найдёт ни одну из них. | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
Итоги: | Итоги: | ||
- | * Полный перебор входных данных | + | * Полный перебор входных данных --- невозможен |
* Полнота покрытия кода не гарантирует правильности | * Полнота покрытия кода не гарантирует правильности | ||
- | + | !! Полнота вычислений | |
==== Реактивные программы ==== | ==== Реактивные программы ==== | ||
- | Кроме традиционных программ, которые завершаются по окончании работы, описываются в терминах «вход/выход» и число состояний которых зависит только от входных данных и переменных, также существуют так называемые реактивные программы. | ||
- | |||
Эти программы работают в бесконечном цикле и взаимодействуют с окружением. Эти программы работают в терминах стимул/реакция. Здесь и возникает цепочка взаимодействия, которая резко увеличивает количество состояний системы, и обойти их тестированием не представляется возможным. | Эти программы работают в бесконечном цикле и взаимодействуют с окружением. Эти программы работают в терминах стимул/реакция. Здесь и возникает цепочка взаимодействия, которая резко увеличивает количество состояний системы, и обойти их тестированием не представляется возможным. | ||
- | Реактивные программы это не пыльный ... на задворках программистких технологий, и | + | Реактивные программы это не пыльный ... на задворках программистких технологий, и ошбики там гораздо менее очевидны. Пример --- системы с разделением ресурсов. |
- | + | == Системы с разделением ресурсов == | |
- | * Дорожный | + | * Дорожный траффик. Пример с дедлоком на перекрёстке |
* Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка. | * Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка. | ||
* ОС. Пример с дедлоком | * ОС. Пример с дедлоком | ||
* ... | * ... | ||
- | + | == Параллельные системы == | |
Новый источник ошибок --- совместная работа проверенных компонентов. | Новый источник ошибок --- совместная работа проверенных компонентов. | ||
Строка 144: | Строка 128: | ||
Дополнительную сложность вносит одновременная работа. | Дополнительную сложность вносит одновременная работа. | ||
- | + | == Доказательство теорем == | |
Есть система, свойства, есть аксиомы и правила вывода, и с помощью последних доказываются свойства. | Есть система, свойства, есть аксиомы и правила вывода, и с помощью последних доказываются свойства. | ||
- | + | Фото 3: проверить свойство, верно ли, что за a выполнится с? С помощью правил вывода мы можем показать, что правило выполняется. | |
- | + | К достоинствам относится тот факт, что можно доказывать для систем с бесконечным количеством состояний. Также даёт более глубокое понимание системы, даже более глубокое, чем нужно. | |
- | + | Недостатки: медленная работа, требуется помощь человека, неполнота аксиом в общем случае | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | == Статический анализ == | |
+ | * Анализ текста программы без его выполнения. Можно сказать, что здесь обходим граф потока управления. В общем случае задача достижимости неразрешима, и в общем случае статический анализ представляет компромисс между возможностями и потребностями. Кроме того, удобные инженерные конструкции очень плохо поддаются статическому анализу. | ||
- | + | Однако есть достаточно узкие области, где статический анализ хорошо применим. | |
- | + | ||
- | + | ||
- | + | ||
- | + | Расширяем множество значениий m неиниц сост. | |
- | + | Начальное сост. --- неиниц. И далее вычисляем отображение для каждой точки программы. | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | Начальное | + | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | Видим, что | + | Видим, что перем. иниц. только при размере массива больше 0. |
- | + | Достоинства статического моделирования: высокая скорость; ответу, если он дан, можно верить. Из минусов --- узкая область применения, а также ручная настройка при изменении проверяемых свойств. | |
- | + | == Верификация программ на моделях == | |
[[Изображение:Savenkov 1.jpg|thumb|240px|left]] | [[Изображение:Savenkov 1.jpg|thumb|240px|left]] | ||
Можно построить модель с конечным количеством состояний, сформулировать свойства, последовательность значений предикатов и выполнить поиск по прост. состояниям, что даст ответ на вопрос, выполняются свойства или нет. Доказывается, что либо свойства выполняются на всех состояниях модели, либо свойства не выполняются. | Можно построить модель с конечным количеством состояний, сформулировать свойства, последовательность значений предикатов и выполнить поиск по прост. состояниям, что даст ответ на вопрос, выполняются свойства или нет. Доказывается, что либо свойства выполняются на всех состояниях модели, либо свойства не выполняются. | ||
Строка 215: | Строка 157: | ||
Итого 4 состояния. | Итого 4 состояния. | ||
- | Контрпример | + | Контрпример --- ошибка в процессе. Нашли ошибку. |
Процесс верификации состоит из 3 этапов: | Процесс верификации состоит из 3 этапов: | ||
* Моделирование. Строим адекватную корректную модель. Цель моделирования --- объяснить. У нас есть программа, есть инструментальное средство верификации. У него есть свой язык. Иногда это делается путём трансляции с языка написания программы на входной язык средства. Но при этом может получиться слишком сложная модель. Тогда необходима абстракция, которая упрощает модель. Модель при этом должна быть корректной и адекватной. Более детально это будет рассматриваться на следующих лекциях. Корректная модель корректно моделирует, а адекватная корректно экстраполирует свойства на систему. Поскольку мы от чего-то абстрагируемся, оставляя то, что нужно, нужно знать, что нужно; модель без задачи не имеет смысла. Но обычно здесь формулируется класс свойств, например, корректна ли программа работает с разделяемыми ресурсами. Тогда построим модель программы, которая работает с разделяемыми ресурсами, от остального абстрагируемся. | * Моделирование. Строим адекватную корректную модель. Цель моделирования --- объяснить. У нас есть программа, есть инструментальное средство верификации. У него есть свой язык. Иногда это делается путём трансляции с языка написания программы на входной язык средства. Но при этом может получиться слишком сложная модель. Тогда необходима абстракция, которая упрощает модель. Модель при этом должна быть корректной и адекватной. Более детально это будет рассматриваться на следующих лекциях. Корректная модель корректно моделирует, а адекватная корректно экстраполирует свойства на систему. Поскольку мы от чего-то абстрагируемся, оставляя то, что нужно, нужно знать, что нужно; модель без задачи не имеет смысла. Но обычно здесь формулируется класс свойств, например, корректна ли программа работает с разделяемыми ресурсами. Тогда построим модель программы, которая работает с разделяемыми ресурсами, от остального абстрагируемся. | ||
- | * Спецификация свойств. Это темпоральная логика плюс | + | * Спецификация свойств. Это темпоральная логика плюс сс нккоторыми добавками, которые использует Spin. Вопрос полноты свойств здесь не затрагивается. Это вопрос валидации и мы считаем, что свойства полны. |
- | * Верификация. Мы передаём модель и свойства в инстр. систему, нажимаем на кнопку проверить, и получаем контрпример. Дальше нужно понять, о чём контрпример говорит, анализ контрпримеров --- это прерогатива человека, | + | * Верификация. Мы передаём модель и свойства в инстр. систему, нажимаем на кнопку проверить, и получаем контрпример. Дальше нужно понять, о чём контрпример говорит, анализ контрпримеров --- это прерогатива человека, котрый разбирается, что произошло: некорректная модель, модель не подходит для свойств, неправильная модель. Однако, если контрпример подтверждается, то мы нашли ошибку. Исправляем её и запускаем заново. Если модель конечная адекватна, то мы гарантированно получим ответ. Она позволяет выялвять редкие ошибки, которые обычно тестированием не выявляются. |
Недостаток: работает только для конечных моделей. Бывают такие программы и свойства, которые нельзя проверить с помощью конечной модели. Если кто-то захочет проверить самоприменимость, то никакая верификация не поможет. | Недостаток: работает только для конечных моделей. Бывают такие программы и свойства, которые нельзя проверить с помощью конечной модели. Если кто-то захочет проверить самоприменимость, то никакая верификация не поможет. | ||
== Автоматизируемость == | == Автоматизируемость == | ||
- | * Автоматизированное тестирование | + | * Автоматизированное тестирование --- автоматизированное выполнение тестов, это было давно. Автоматического тестирования нет. |
- | * Доказательство теорем | + | * Доказательство теорем --- участие человека существенно |
* Статический анализ полностью автомат. в данной области и для данного свойства | * Статический анализ полностью автомат. в данной области и для данного свойства | ||
* Верификация - участие человека сводится к построению модели и анализу контрпримеров. Проблема --- комбинаторный взрыв. | * Верификация - участие человека сводится к построению модели и анализу контрпримеров. Проблема --- комбинаторный взрыв. | ||
Строка 243: | Строка 185: | ||
* Варди и Вольпер, 1986 -- анализ конформности в model checking, это снимает ограничение на конечность числа состояний. | * Варди и Вольпер, 1986 -- анализ конформности в model checking, это снимает ограничение на конечность числа состояний. | ||
В основном курсе будет уделять ся первому моделчекингу | В основном курсе будет уделять ся первому моделчекингу | ||
- | * Хольцман, | + | * Хольцман, 1981. Построен верификатор Spin |
=== Проблема комбинаторного взрыва === | === Проблема комбинаторного взрыва === |