ВПнМ, 01 лекция (от 08 февраля)

Материал из eSyr's wiki.

(Различия между версиями)
Перейти к: навигация, поиск
(Параллельные системы)
Текущая версия (16:59, 14 сентября 2010) (править) (отменить)
(Развитие методов)
 
(17 промежуточных версий не показаны.)
Строка 1: Строка 1:
 +
'''Оригинальная презентация:''' http://savenkov.lvk.cs.msu.su/mc/lect1.ppt
 +
Верификация программ на моделях, Верификация моделей программ, Model checking.
Верификация программ на моделях, Верификация моделей программ, Model checking.
Строка 18: Строка 20:
Эта лекция вводная. Лектор расскажет, что такое правильность программ, почему её надо проверять строгими методами. Сделает небольшой обзор методов проверки правильности программ, расскажет, как развивалась эта область, и то, как будет устроен практикум и зачёт по этому курсу. Будет экзамен. Зачёт лектор отменил, допущены будут все.
Эта лекция вводная. Лектор расскажет, что такое правильность программ, почему её надо проверять строгими методами. Сделает небольшой обзор методов проверки правильности программ, расскажет, как развивалась эта область, и то, как будет устроен практикум и зачёт по этому курсу. Будет экзамен. Зачёт лектор отменил, допущены будут все.
-
==Разработка программы ==
+
== Разработка программы ==
Ошибки появляются в ходе разработки программы. Существуют различные модели жизненного цикла, но можно выделить основные этапы:
Ошибки появляются в ходе разработки программы. Существуют различные модели жизненного цикла, но можно выделить основные этапы:
Строка 24: Строка 26:
* Проектирование, в ходе которого разрабатывается архитектура системы
* Проектирование, в ходе которого разрабатывается архитектура системы
* Реализация
* Реализация
-
* Темтированик
+
* Тестирование
-
* Эксплуатация, в ходе которой внедряется система, исопльзуется
+
* Эксплуатация, в ходе которой внедряется система, используется
Ошибки могут появляться на всех этих этапах. В ходе анализа можно не так понять пользователя, в ходе разработки архитектуры, есть ошибки в ходе тестирования и эксплуатации.
Ошибки могут появляться на всех этих этапах. В ходе анализа можно не так понять пользователя, в ходе разработки архитектуры, есть ошибки в ходе тестирования и эксплуатации.
-
Наибольшее количество ошибок вносится на этапах проектирования и реализации. Обнаруживаются на этапе тестирования, особенно сборочного. Выглядит всё неплохо, но цена ошибки резко возврастает в ходе эксплуатации.
+
Наибольшее количество ошибок вносится на этапах проектирования и реализации. Обнаруживаются на этапе тестирования, особенно сборочного. Выглядит всё неплохо, но цена ошибки резко возрастает в ходе эксплуатации.
== Правильность программ ==
== Правильность программ ==
Строка 41: Строка 43:
Все другие ошибки, которые есть, выявляются во время разработки программы. Процесс поиска этих ошибок --- процесс верификации: проверка, соответствует ли реализация спецификации. При этом считается, что спецификация правильная.
Все другие ошибки, которые есть, выявляются во время разработки программы. Процесс поиска этих ошибок --- процесс верификации: проверка, соответствует ли реализация спецификации. При этом считается, что спецификация правильная.
-
В ходе верификации/валидвции нужно найти ошибки, или доказать, что их нет.
+
В ходе верификации/валидации нужно найти ошибки, или доказать, что их нет.
Когда средство создаётся, средств на тестирование обычно нет. Но существуют другие системы, в которых ошибок не должно быть ни при каких обстоятельствах. Это системы с повышенными требованиями к надёжности. Это системы либо с большой ценой ошибки, либо приводящие к невосполнимым потерям.
Когда средство создаётся, средств на тестирование обычно нет. Но существуют другие системы, в которых ошибок не должно быть ни при каких обстоятельствах. Это системы с повышенными требованиями к надёжности. Это системы либо с большой ценой ошибки, либо приводящие к невосполнимым потерям.
Строка 56: Строка 58:
Задача верификации программ в общем случае алгоритмически неразрешима. Таким образом, применение формальных методов, несмотря на общее мнение, что там что-то доказывается, что невозможно, там приводится обоснование, что их нет.
Задача верификации программ в общем случае алгоритмически неразрешима. Таким образом, применение формальных методов, несмотря на общее мнение, что там что-то доказывается, что невозможно, там приводится обоснование, что их нет.
-
В абсолютном большинстве встречающиеся в природе системы таковы, что их ошибочность можно доказать, и это признак хорошего дизайна. По англицки это называется probably correct.
+
В абсолютном большинстве встречающиеся в природе системы таковы, что их ошибочность можно доказать, и это признак хорошего дизайна. По английcки это называется probably correct.
== Формальные методы ==
== Формальные методы ==
-
ФМ --- использование матаппарата, реализованного в языках, методах и средствах спецификации и верификации программ.
+
ФМ использование математического аппарата, реализованного в языках, методах и средствах спецификации и верификации программ.
* Методы формальной спецификации
* Методы формальной спецификации
Строка 80: Строка 82:
* Проверяется та программа, которая будет использоваться
* Проверяется та программа, которая будет использоваться
* Для проведения теста не требуется дополнительных инструментальных средств
* Для проведения теста не требуется дополнительных инструментальных средств
-
* Удобная локализация ошибки. Средства тетстирования и отладки очень хорошо позволяют найти место в коде, где она находится
+
* Удобная локализация ошибки. Средства тестирования и отладки очень хорошо позволяют найти место в коде, где она находится
Минусы:
Минусы:
* Не всегда есть условия для тестирования системы
* Не всегда есть условия для тестирования системы
-
* Проблема с воспроизводимостью тестов. Ошибка должна быть воспроизводима для понимания и отладки. Если речь идёт про системы взаимодействия с реальным окружением или когда она связана с историей взаимодействия, то в этих случаях ошибка может быть невоспроизводима.
+
* Проблема с воспроизводимостью тестов. Ошибка должна быть воспроизводима для понимания и отладки. Если речь идёт про системы взаимодействия с реальным окружением или когда она связана с историей взаимодействия, то в этих случаях ошибка может быть не воспроизводима.
Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д.
Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д.
Строка 90: Строка 92:
* ЧЯ: для последовательных программ сложно перебрать все входные данные
* ЧЯ: для последовательных программ сложно перебрать все входные данные
* ЧЯ: для параллельных дополнительно возникают цепочки взаимодействия и перестановки
* ЧЯ: для параллельных дополнительно возникают цепочки взаимодействия и перестановки
-
* ЧЯ: для динамических структур, взаимодейсьвующих с окружением --- невозможно
+
* ЧЯ: для динамических структур, взаимодействующих с окружением --- невозможно
* ПЯ: большой размер покрытия, растёт экспоненциально с размером
* ПЯ: большой размер покрытия, растёт экспоненциально с размером
-
* Часто невозможно построение 100% покрытия.
+
* Часто невозможно построение 100% покрытия, например, в случае наличия недостижимого кода.
-
* Полное покрытие не гарантирует отсутствие ошибков.
+
* Полное покрытие не гарантирует отсутствие ошибок.
Пример: полное покрытие для ЧЯ:
Пример: полное покрытие для ЧЯ:
-
* Поиск выигрышной стратегии в шашках --- 10^14 операций (?)
+
* Поиск выигрышной стратегии в шашках 10<sup>14</sup> операций (?)
-
полное покрытие для прозрачного ящика:
+
Пример невозможности построения полного покрытия для прозрачного ящика:
-
* //пример с ифами
+
int x = 1;
 +
if (x == 1) {
 +
std::cout << "Okay" << std::endl;
 +
} else {
 +
std::cout << "Error" << std::endl;
 +
}
 +
Для этой программы нельзя построить полное покрытие — ветвь else ни при каких условиях не выполнится.
-
Для программы 1 нельзя построить полное покрытие
+
Полное тестовое покрытие — не панацея. Пусть у нас имеется функция с двумя ошибками:
-
 
+
int strlen(const char * p) {
-
Для второй программы с двумя ошибками можно построить покрытие a, bbb, но оно не найдёт ни одну из них.
+
int len = 0;
 +
do {
 +
++len;
 +
} while (*p++);
 +
return len;
 +
}
 +
Для неё можно построить покрытие "a", "bbb", но оно не выявит ни одну из ошибок.
Итоги:
Итоги:
-
* Полный перебор входных данных --- невозможен
+
* Полный перебор входных данных невозможен
* Полнота покрытия кода не гарантирует правильности
* Полнота покрытия кода не гарантирует правильности
-
!! Полнота вычислений
+
<!-- Кто помнит, к чему это? --- !! Полнота вычислений -->
==== Реактивные программы ====
==== Реактивные программы ====
 +
Кроме традиционных программ, которые завершаются по окончании работы, описываются в терминах «вход/выход» и число состояний которых зависит только от входных данных и переменных, также существуют так называемые реактивные программы.
 +
Эти программы работают в бесконечном цикле и взаимодействуют с окружением. Эти программы работают в терминах стимул/реакция. Здесь и возникает цепочка взаимодействия, которая резко увеличивает количество состояний системы, и обойти их тестированием не представляется возможным.
Эти программы работают в бесконечном цикле и взаимодействуют с окружением. Эти программы работают в терминах стимул/реакция. Здесь и возникает цепочка взаимодействия, которая резко увеличивает количество состояний системы, и обойти их тестированием не представляется возможным.
-
Реактивные программы это не пыльный ... на задворках программистких технологий, и ошбики там гораздо менее очевидны. Пример --- системы с разделением ресурсов.
+
Реактивные программы это не пыльный ... на задворках программистких технологий, и ошибки там гораздо менее очевидны. Пример системы с разделением ресурсов.
-
== Системы с разделением ресурсов ==
+
==== Системы с разделением ресурсов ====
-
* Дорожный траффик. Пример с дедлоком на перекрёстке
+
* Дорожный трафик. Пример с дедлоком на перекрёстке
* Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка.
* Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка.
* ОС. Пример с дедлоком
* ОС. Пример с дедлоком
* ...
* ...
-
== Параллельные системы ==
+
==== Параллельные системы ====
Новый источник ошибок --- совместная работа проверенных компонентов.
Новый источник ошибок --- совместная работа проверенных компонентов.
Строка 128: Строка 144:
Дополнительную сложность вносит одновременная работа.
Дополнительную сложность вносит одновременная работа.
-
== Доказательство теорем ==
+
=== Доказательство теорем ===
-
Есть система, свойства, есть аксиомы иправила вывода, и с помощью последних доказываются свойства.
+
Есть система, свойства, есть аксиомы и правила вывода, и с помощью последних доказываются свойства.
 +
 
 +
Пример:
-
Фото 3: проверить свойство, верно ли, что за a выполнится с? С помощью правил вывода мы можем показать, что правило выполняется.
+
Пусть у нас имеется система:
 +
* <math>A = c \bullet a \bullet B</math>
 +
* <math>B = b \bullet A</math>
 +
И нам необходимо проверить свойство:
 +
* <math>a \bullet c</math> ?
 +
то есть, выполнится ли ''c'' после ''a''. Используя следующие правила вывода:
 +
* <math>\frac{S_1 = a_1 \bullet S_2 \or S_2 = a_2 \bullet S_3}{S_1 = a_1 \bullet a_2 \bullet S_3}</math>
 +
* <math>\frac{s_1 \bullet s_2 \or s_2 \bullet s_3}{s_1 \bullet s_3}</math>
 +
С помощью этих правил вывода мы можем показать, что правило выполняется.
-
К достоинствам относится тот факт, что можно доказывать для систем с беск. кол. сост. Также даёт более глубокое понимание системы, даже более глубокое, чем нужно.
+
К '''достоинствам''' относится тот факт, что можно доказывать свойства для систем с бесконечным количеством состояний. Также этот подход даёт более глубокое понимание системы, даже более глубокое, чем нужно.
-
Недостатки: меделнная работа, требуется помощь человека, неполнота аксиом в общем случае
+
-
== Статический анализ ==
+
'''Недостатки''': медленная работа, требуется помощь человека, неполнота аксиом в общем случае.
-
* Анализ текста программы без его выполнения. Можно сказать, что здесь обходим граф потока управления. В общем случае задача достижимости неразрешима, и в общем случае стат. анализ представляет компромисс между возм. и потребностями. Кроме того, удобные инженерные конструкции очень плохо поддаются статич. анализу.
+
-
Однако есть достаточно узкие области, где стат. анализ хорошо применим.
+
=== Статический анализ ===
 +
* Анализ текста программы без его выполнения. Можно сказать, что здесь обходим граф потока управления. В общем случае задача достижимости неразрешима, и в общем случае статический анализ представляет компромисс между возможностями и потребностями. Кроме того, удобные инженерные конструкции очень плохо поддаются статическому анализу.
-
Расширяем множество значениий m неиниц. сост.
+
Однако есть достаточно узкие области, где статический анализ хорошо применим. Рассмотрим пример:
-
Начальное сост. --- неиниц. И далее вычисляем отображение для каждой точки программы.
+
int min(int * arr, int n) {
 +
int m;
 +
if (n > 0) {
 +
m = arr[0];
 +
} //&larr;
 +
int i = 0;
 +
while (i < n) {
 +
if (m > arr[i]) {
 +
m = arr[i];
 +
}
 +
i++;
 +
}
 +
return m;
 +
}
 +
Проверим, инициализирована ли переменная m в месте, отмеченном стрелочкой. Для этого расширяем множество значениий m неинициализированным состоянием (еще можно посмотреть [[Введение в теорию построения оптимизирующих компиляторов, 04 лекция (от 24 октября)|эту лекцию]] [[Введение в теорию построения оптимизирующих компиляторов|спецкурса Чернова]] — [[Участник:83.237.57.184|83.237.57.184]]):
 +
: dom(m) = Int + { &omega; } — возможные состояния m — множество значений Int и «пустое» состояние
 +
: NI = { &omega; } — неинициализированные состояния — пустое состояние
 +
: I = Int — инициализированные состояния — состояние из множества Int
 +
* v = Expr &rarr; {NI, I} — возможные состояния в данной точке программы
 +
Начальное состояние — неинициализированное. И далее вычисляем отображение для каждой точки программы.
 +
int min(int * arr, int n) {
 +
int m; < v = { NI } >
 +
if (n > 0) { < v = { NI } >
 +
m = arr[0]; < v = { I } >
 +
} //&larr; < v = { NI, I } > (!)
 +
int i = 0; < v = { NI, I } >
 +
while (i < n) { < v = { NI, I } >
 +
if (m > arr[i]) { < v = { NI, I } >
 +
m = arr[i]; < v = { I } >
 +
}
 +
i++; < v = { NI, I } >
 +
}
 +
return m; < v = { NI, I } >
 +
}
-
Видим, что перем. иниц. только при размере массива больше 0.
+
Видим, что переменная инициализируется только при размере массива больше 0.
-
Достоинства стат. мод.: высокая скорость, ответу, если он дан, можно верить. Из минусов --- узкая обл. применения, а также ручная настройка при изм. проверяемых свойств.
+
'''Достоинства''' статического моделирования: высокая скорость; ответу, если он дан, можно верить. Из '''минусов''' — узкая область применения, а также ручная настройка при изменении проверяемых свойств.
-
== Верификация программ на моделях ==
+
=== Верификация программ на моделях ===
[[Изображение:Savenkov 1.jpg|thumb|240px|left]]
[[Изображение:Savenkov 1.jpg|thumb|240px|left]]
-
Можно построить модель с конеяч. кол. сост., сформулировать свойства, послед знач. предикатов и выполнить поиск по прост. сост., что дасто ответ на вопрос, выполняются свойства или нет. Доказывается, что либо свойства вып. на всех сост. модели, либо свойство не вып.
+
Можно построить модель с конечным количеством состояний, сформулировать свойства, последовательность значений предикатов и выполнить поиск по прост. состояниям, что даст ответ на вопрос, выполняются свойства или нет. Доказывается, что либо свойства выполняются на всех состояниях модели, либо свойства не выполняются.
Что нам важно:
Что нам важно:
-
* программа может наход. в сост. открыта/закрыта
+
* программа может находится в состоянии открыта/закрыта
-
* Сост. меняются в двух местах
+
* Состояния меняются в двух местах
Итого 4 состояния.
Итого 4 состояния.
-
Контрпример --- ошибка в процессе. Нашли ошибку.
+
Контрпример ошибка в процессе. Нашли ошибку.
-
Процесс вериф. сост. из 3 этапов:
+
Процесс верификации состоит из 3 этапов:
-
* Моделирование. Строим адекватную корректную модель. Цель моделирования --- объяснить. У нас есть программа, есть инструментальное средство вериф. У него есть свой язык. Иногда это делается путём трансляции с языка напис. программы на вх. язык средства. Но при этом может получиться слишком сложная модель. Тогда необходима абстракция, которая упрощает можель. Модель при этом должна быть корректной и адекватной. Более детально это будет рассм. на след. лекциях. Коррект. моель корректно моделирует., а адекватная корректно экстраполирует св-ва на систему. Поскольку мы от чего-то абстрагируемся, оставляя то, что нужно, нужно знать, что нужно; модель без задачи не имеет смысла. Но обычно здесь формулируется класс свойств, например, корректна ли программа работает с разделяемыми ресурсами. тогда построим модель программы, которая работает с разд. рес., от остального абстрагируемся.
+
* Моделирование. Строим адекватную корректную модель. Цель моделирования --- объяснить. У нас есть программа, есть инструментальное средство верификации. У него есть свой язык. Иногда это делается путём трансляции с языка написания программы на входной язык средства. Но при этом может получиться слишком сложная модель. Тогда необходима абстракция, которая упрощает модель. Модель при этом должна быть корректной и адекватной. Более детально это будет рассматриваться на следующих лекциях. Корректная модель корректно моделирует, а адекватная корректно экстраполирует свойства на систему. Поскольку мы от чего-то абстрагируемся, оставляя то, что нужно, нужно знать, что нужно; модель без задачи не имеет смысла. Но обычно здесь формулируется класс свойств, например, корректна ли программа работает с разделяемыми ресурсами. Тогда построим модель программы, которая работает с разделяемыми ресурсами, от остального абстрагируемся.
-
* Спецификация свойств. Это темпоральная логика плюс сс нккоторыми добавками, которые исп. Spin. Вопрос полноты свойств здесь не затрагивается. Это вопрос валидации и мы считаем, что свойства полны.
+
* Спецификация свойств. Это темпоральная логика плюс с некоторыми добавками, которые использует Spin. Вопрос полноты свойств здесь не затрагивается. Это вопрос валидации и мы считаем, что свойства полны.
-
* Верификация. Мы передаём модель и св-ва в инстр. систему, нажимаем на кнопку проверить, и получаем контрпример. Дальше нужно понять, о чём контрпример говорит, анализ кп это прерогатива человека, котрый разбирается, что произошло: некорректная модель, модель не подходит для свойств, неправльная модель. Однако, если контрпример подтверждается, то мы нашли ошибку. Исправляем её и запускаем заново. Если модель конечная адекватна, то мы гарантированно получис ответ. Она позволяет выялвять редкие ошибки, которые обычно тестирование не выявляются.
+
* Верификация. Мы передаём модель и свойства в инстр. систему, нажимаем на кнопку проверить, и получаем контрпример. Дальше нужно понять, о чём контрпример говорит, анализ контрпримеров --- это прерогатива человека, который разбирается, что произошло: некорректная модель, модель не подходит для свойств, неправильная модель. Однако, если контрпример подтверждается, то мы нашли ошибку. Исправляем её и запускаем заново. Если модель конечная адекватна, то мы гарантированно получим ответ. Она позволяет выявлять редкие ошибки, которые обычно тестированием не выявляются.
-
Недостаток: работает только для конечных моделей. Бывают такие программы и св-ва, которые нельзя проверить с помощью конечной модели. Если кто-то захочет проверить самоприменимость, то никакая верификация не поможет.
+
Недостаток: работает только для конечных моделей. Бывают такие программы и свойства, которые нельзя проверить с помощью конечной модели. Если кто-то захочет проверить самоприменимость, то никакая верификация не поможет.
== Автоматизируемость ==
== Автоматизируемость ==
-
* Автоматизированное тестирование --- автомат. вып. тестов, это было давно. Автоматического тестирования нет.
+
* Автоматизированное тестирование — автоматизированное выполнение тестов, это было давно. Автоматического тестирования нет.
-
* Доказательство теорем --- участие человека существенно
+
* Доказательство теорем участие человека существенно
-
* Статич. анализ полностью автомат. в данной области и для данного св-ва
+
* Статический анализ полностью автомат. в данной области и для данного свойства
-
* Верификация - участие человека сводится к постр. модели и анализе контрпримеров. Проблема --- комбинаторный взрыв.
+
* Верификация - участие человека сводится к построению модели и анализу контрпримеров. Проблема --- комбинаторный взрыв.
== История развития ==
== История развития ==
-
* Флойд, 1967. Ф. предложил использовать assertions, и выдвитнул гипотезу, что если у нас для некоторого ЯП описаны ass., то, с учётом того, как влияет оно на вып., можно доказать, что программа корректна
+
* Флойд, 1967. Ф. предложил использовать assertions, и выдвинул гипотезу, что если у нас для некоторого ЯП описаны assertions, то, с учётом того, как влияет оно на выполнение, можно доказать, что программа корректна
-
* Хоар ввёл триплеты (P | S | Q) и ввёл логич. вывод, и в первое время это делалось вручную.
+
* Хоар ввёл триплеты (P | S | Q) и ввёл логический вывод, и в первое время это делалось вручную.
* Первый автоматический прувер --- 1971
* Первый автоматический прувер --- 1971
-
* Дейкстра, 1975 описал язык, который более удачно позволял доказывать корр. программ. Каждому операторы сопоставллялся guard, причём если было условие, то гарды выполнялись недетерменированно.
+
* Дейкстра, 1975 описал язык, который более удачно позволял доказывать корректность программ. Каждому оператору сопоставлялся guard, причём если было условие, то гарды выполнялись недетерменированно.
-
* Хоар, 1978 описал CSP --- взаимод. посл. процессы, это позв. доказывать корр. распред. программ
+
* Хоар, 1978 описал CSP --- взаимодействующие последовательно процессы, это позволило доказывать корректность распределенных программ
=== Развитие методов ===
=== Развитие методов ===
-
* Пнуэли, 1977 --- темпоральная логика, LTL. Стало возм. описывать свойства подмножеством языка и выполнимость словами языка (?)
+
* Пнуэли, 1977 --- темпоральная логика, LTL. Стало возможным описывать свойства подмножеством языка и выполнимость словами языка (?)
-
* Пнуэли, 1981 --- предложена логика ветвящегося времени, которая лучше подходит для тонких св-в пар. программ
+
* Пнуэли, 1981 --- предложена логика ветвящегося времени, которая лучше подходит для тонких свойств параллельных программ
-
* Клар, Эмерсон, 1981 --- предложен model checking, когда предст. программу в виде автомата с конеч. чслом сост., обходим дост. сост. и проверяем св-ва.
+
* Клар, Эмерсон, 1981 --- предложен model checking, когда представляет программу в виде автомата с конечным числом состояний, обходим достижимые состояния и проверяем свойства.
-
* Варди и Вольпер, 1986 -- анализ комформности в model checking, это снимает огр. на конеч. число сост.
+
* Варди и Вольпер, 1986 -- анализ конформности в model checking, это снимает ограничение на конечность числа состояний.
В основном курсе будет уделять ся первому моделчекингу
В основном курсе будет уделять ся первому моделчекингу
-
* Хольцман, 1981. Построен верификатор Spin
+
* Хольцман, 1989. Построен верификатор Spin
=== Проблема комбинаторного взрыва ===
=== Проблема комбинаторного взрыва ===
-
* Бриан, 1989. Двоичные решающие диаграммы (BDD) --- мы строим пространство сост., и склеиваем ветви согласно ряду правил
+
* Бриан, 1989. Двоичные решающие диаграммы (BDD) --- мы строим пространство состояний, и склеиваем ветви согласно ряду правил
-
* МакМиллан, 1993. Верификатор SMV, исп. BDD
+
* МакМиллан, 1993. Верификатор SMV, использующий BDD
-
* Хольцман, Пелед, 1994 --- верификация паралл. систем.. Довольно часто бывает так, что порядок обмена не важен, тогда можно рассм. один из возможных --- редукция част. порядков
+
* Хольцман, Пелед, 1994 --- верификация параллельных систем.. Довольно часто бывает так, что порядок обмена не важен, тогда можно рассмотреть один из возможных --- редукция част. порядков
* 1995. Редукция част. порядков в Spin
* 1995. Редукция част. порядков в Spin
-
после этого стало возм. применять верификаторы в промышленности.
+
После этого стало возможным применять верификаторы в промышленности.
=== Дальнейшее развитие ===
=== Дальнейшее развитие ===
Было направлено на решение задачи комбинаторного взрыва
Было направлено на решение задачи комбинаторного взрыва
-
* Кларк, 1992 --- абстракцичя для уменьш. модели
+
* Кларк, 1992 --- абстракция для уменьшения модели
-
* Эльсаиди, 1994 --- семант. минимиз
+
* Эльсаиди, 1994 --- семантическая минимизация
-
* Пелед, 1996 Бир, 1998 --- вериф. на лету, подгрузка по мере анализа и удаление просм. куска дерева из памяти
+
* Пелед, 1996 Бир, 1998 --- верификация на лету, подгрузка по мере анализа и удаление просмотренного куска дерева из памяти
-
* Расси, 2000 - анализ достижимости с учётом специф. --- выбор эвристики на осн. св-в
+
* Расси, 2000 - анализ достижимости с учётом спецификации --- выбор эвристики на основании свойств
* Эмерсон и Прасад, 1994 --- симметрия
* Эмерсон и Прасад, 1994 --- симметрия
-
== Области применения вериф. на моделях ==
+
== Области применения верификации на моделях ==
-
* Сетевые и криптограф. протоколы
+
* Сетевые и криптографические протоколы
* Протоколы работы кэш-памяти
* Протоколы работы кэш-памяти
-
* Инт. схемы
+
* Интегральные схемы
* Стандарты
* Стандарты
* Встроенные системы
* Встроенные системы
* Драйвера
* Драйвера
-
* Вообще программы на С. Для Spic есть конвертер из C в его внутр. язык
+
* Вообще программы на С. Для Spin есть конвертер из C в его внутренний язык
{{ВПнМ}}
{{ВПнМ}}
{{Lection-stub}}
{{Lection-stub}}

Текущая версия

Оригинальная презентация: http://savenkov.lvk.cs.msu.su/mc/lect1.ppt

Верификация программ на моделях, Верификация моделей программ, Model checking.

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

В качестве инструментального средства будем использовать программу Spin.

По курсу будет практикум, проходить он будет в 758 комнате.

Содержание

[править] План лекции

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

Эта лекция вводная. Лектор расскажет, что такое правильность программ, почему её надо проверять строгими методами. Сделает небольшой обзор методов проверки правильности программ, расскажет, как развивалась эта область, и то, как будет устроен практикум и зачёт по этому курсу. Будет экзамен. Зачёт лектор отменил, допущены будут все.

[править] Разработка программы

Ошибки появляются в ходе разработки программы. Существуют различные модели жизненного цикла, но можно выделить основные этапы:

  • Анализ
  • Проектирование, в ходе которого разрабатывается архитектура системы
  • Реализация
  • Тестирование
  • Эксплуатация, в ходе которой внедряется система, используется

Ошибки могут появляться на всех этих этапах. В ходе анализа можно не так понять пользователя, в ходе разработки архитектуры, есть ошибки в ходе тестирования и эксплуатации.

Наибольшее количество ошибок вносится на этапах проектирования и реализации. Обнаруживаются на этапе тестирования, особенно сборочного. Выглядит всё неплохо, но цена ошибки резко возрастает в ходе эксплуатации.

[править] Правильность программ

Что такое ошибка? Ошибка --- несоответствие требованиям. Если нет требований к программе, то нет неправильности. Программа не может быть ни правильной, ни неправильной в таком случае, она может быть забавной.

Ошибки бывают в формулировке требований и в их соблюдении.

Ошибки в формулировке: реализовано вроде всё правильно, а пользователь скажет, что здесь ошибка. Такие ошибки выявляются в ходе процесса, называемого валидация.

Все другие ошибки, которые есть, выявляются во время разработки программы. Процесс поиска этих ошибок --- процесс верификации: проверка, соответствует ли реализация спецификации. При этом считается, что спецификация правильная.

В ходе верификации/валидации нужно найти ошибки, или доказать, что их нет.

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

Примеры:

  • Ariana-5. Июнь 1996, взрыв ракеты спустя 40 секунд после старта. Ущерб --- 500 млн., стоимость разработки --- 7 млрд., причина ошибки: преобразования 64-bit float в 16-bit int
  • Patriot: округление 24-bit fixed
  • Sleipner A. Причина — ошибка округления при моделировании платформы.

Соответственно, для проверки правильности систем с повышенными требованиями к надёжности выборочное тестирование не подходит, и, как сказал Дейкстра, тестирование может выявить ошибки, но не показать, что их нет.

Тестирование направлено на выявление частых ошибок. Формальные методы направлены на поиск критических ошибок. Соотвтественно, редкие безвредные ошибки никого не интересуют.

Задача верификации программ в общем случае алгоритмически неразрешима. Таким образом, применение формальных методов, несмотря на общее мнение, что там что-то доказывается, что невозможно, там приводится обоснование, что их нет.

В абсолютном большинстве встречающиеся в природе системы таковы, что их ошибочность можно доказать, и это признак хорошего дизайна. По английcки это называется probably correct.

[править] Формальные методы

ФМ — использование математического аппарата, реализованного в языках, методах и средствах спецификации и верификации программ.

  • Методы формальной спецификации
  • Верификация
    • Доказательство теорем
    • Верификация на моделях

[править] Методы верификации

  • Полное тестирование. Тестирование, в ходе которого при построении тестового набора приводится обоснование, что набор полный.
  • Имитационное тестирование. Это то же тестирование, только оно помогает избежать в том случае, например, если система ещё не готова.
  • Доказательство теорем
  • Статический анализ
  • Верификация на моделях

[править] Тестирование

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

Плюсы:

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

Минусы:

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

Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д.

Обоснование полноты тестового покрытия:

  • ЧЯ: для последовательных программ сложно перебрать все входные данные
  • ЧЯ: для параллельных дополнительно возникают цепочки взаимодействия и перестановки
  • ЧЯ: для динамических структур, взаимодействующих с окружением --- невозможно
  • ПЯ: большой размер покрытия, растёт экспоненциально с размером
  • Часто невозможно построение 100% покрытия, например, в случае наличия недостижимого кода.
  • Полное покрытие не гарантирует отсутствие ошибок.

Пример: полное покрытие для ЧЯ:

  • Поиск выигрышной стратегии в шашках — 1014 операций (?)

Пример невозможности построения полного покрытия для прозрачного ящика:

int x = 1;
if (x == 1) {
  std::cout << "Okay" << std::endl;
} else {
  std::cout << "Error" << std::endl;
}

Для этой программы нельзя построить полное покрытие — ветвь else ни при каких условиях не выполнится.

Полное тестовое покрытие — не панацея. Пусть у нас имеется функция с двумя ошибками:

int strlen(const char * p) {
  int len = 0;
  do {
    ++len;
  } while (*p++);
  return len;
}

Для неё можно построить покрытие "a", "bbb", но оно не выявит ни одну из ошибок.

Итоги:

  • Полный перебор входных данных — невозможен
  • Полнота покрытия кода не гарантирует правильности

[править] Реактивные программы

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

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

Реактивные программы это не пыльный ... на задворках программистких технологий, и ошибки там гораздо менее очевидны. Пример — системы с разделением ресурсов.

[править] Системы с разделением ресурсов

  • Дорожный трафик. Пример с дедлоком на перекрёстке
  • Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка.
  • ОС. Пример с дедлоком
  • ...

[править] Параллельные системы

Новый источник ошибок --- совместная работа проверенных компонентов.

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

Дополнительную сложность вносит одновременная работа.

[править] Доказательство теорем

Есть система, свойства, есть аксиомы и правила вывода, и с помощью последних доказываются свойства.

Пример:

Пусть у нас имеется система:

  • A = c \bullet a \bullet B
  • B = b \bullet A

И нам необходимо проверить свойство:

  • a \bullet c ?

то есть, выполнится ли c после a. Используя следующие правила вывода:

  • \frac{S_1 = a_1 \bullet S_2 \or S_2 = a_2 \bullet S_3}{S_1 = a_1 \bullet a_2 \bullet S_3}
  • \frac{s_1  \bullet s_2 \or s_2 \bullet s_3}{s_1 \bullet s_3}

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

К достоинствам относится тот факт, что можно доказывать свойства для систем с бесконечным количеством состояний. Также этот подход даёт более глубокое понимание системы, даже более глубокое, чем нужно.

Недостатки: медленная работа, требуется помощь человека, неполнота аксиом в общем случае.

[править] Статический анализ

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

Однако есть достаточно узкие области, где статический анализ хорошо применим. Рассмотрим пример:

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;
}

Проверим, инициализирована ли переменная m в месте, отмеченном стрелочкой. Для этого расширяем множество значениий m неинициализированным состоянием (еще можно посмотреть эту лекцию спецкурса Чернова83.237.57.184):

dom(m) = Int + { ω } — возможные состояния m — множество значений Int и «пустое» состояние
NI = { ω } — неинициализированные состояния — пустое состояние
I = Int — инициализированные состояния — состояние из множества Int
  • v = Expr → {NI, I} — возможные состояния в данной точке программы

Начальное состояние — неинициализированное. И далее вычисляем отображение для каждой точки программы.

int min(int * arr, int n) {
  int m;               < v = { NI } >
  if (n > 0) {         < v = { NI } >
    m = arr[0];        < v = { I } >
  } //←                < v = { NI, I } > (!)
  int i = 0;           < v = { NI, I } >
  while (i < n) {      < v = { NI, I } >
    if (m > arr[i]) {  < v = { NI, I } >
      m = arr[i];      < v = { I } >
    }
    i++;               < v = { NI, I } >
  }
  return m;            < v = { NI, I } >
}

Видим, что переменная инициализируется только при размере массива больше 0.

Достоинства статического моделирования: высокая скорость; ответу, если он дан, можно верить. Из минусов — узкая область применения, а также ручная настройка при изменении проверяемых свойств.

[править] Верификация программ на моделях

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

Что нам важно:

  • программа может находится в состоянии открыта/закрыта
  • Состояния меняются в двух местах

Итого 4 состояния.

Контрпример — ошибка в процессе. Нашли ошибку.

Процесс верификации состоит из 3 этапов:

  • Моделирование. Строим адекватную корректную модель. Цель моделирования --- объяснить. У нас есть программа, есть инструментальное средство верификации. У него есть свой язык. Иногда это делается путём трансляции с языка написания программы на входной язык средства. Но при этом может получиться слишком сложная модель. Тогда необходима абстракция, которая упрощает модель. Модель при этом должна быть корректной и адекватной. Более детально это будет рассматриваться на следующих лекциях. Корректная модель корректно моделирует, а адекватная корректно экстраполирует свойства на систему. Поскольку мы от чего-то абстрагируемся, оставляя то, что нужно, нужно знать, что нужно; модель без задачи не имеет смысла. Но обычно здесь формулируется класс свойств, например, корректна ли программа работает с разделяемыми ресурсами. Тогда построим модель программы, которая работает с разделяемыми ресурсами, от остального абстрагируемся.
  • Спецификация свойств. Это темпоральная логика плюс с некоторыми добавками, которые использует Spin. Вопрос полноты свойств здесь не затрагивается. Это вопрос валидации и мы считаем, что свойства полны.
  • Верификация. Мы передаём модель и свойства в инстр. систему, нажимаем на кнопку проверить, и получаем контрпример. Дальше нужно понять, о чём контрпример говорит, анализ контрпримеров --- это прерогатива человека, который разбирается, что произошло: некорректная модель, модель не подходит для свойств, неправильная модель. Однако, если контрпример подтверждается, то мы нашли ошибку. Исправляем её и запускаем заново. Если модель конечная адекватна, то мы гарантированно получим ответ. Она позволяет выявлять редкие ошибки, которые обычно тестированием не выявляются.

Недостаток: работает только для конечных моделей. Бывают такие программы и свойства, которые нельзя проверить с помощью конечной модели. Если кто-то захочет проверить самоприменимость, то никакая верификация не поможет.

[править] Автоматизируемость

  • Автоматизированное тестирование — автоматизированное выполнение тестов, это было давно. Автоматического тестирования нет.
  • Доказательство теорем — участие человека существенно
  • Статический анализ полностью автомат. в данной области и для данного свойства
  • Верификация - участие человека сводится к построению модели и анализу контрпримеров. Проблема --- комбинаторный взрыв.

[править] История развития

  • Флойд, 1967. Ф. предложил использовать assertions, и выдвинул гипотезу, что если у нас для некоторого ЯП описаны assertions, то, с учётом того, как влияет оно на выполнение, можно доказать, что программа корректна
  • Хоар ввёл триплеты (P | S | Q) и ввёл логический вывод, и в первое время это делалось вручную.
  • Первый автоматический прувер --- 1971
  • Дейкстра, 1975 описал язык, который более удачно позволял доказывать корректность программ. Каждому оператору сопоставлялся guard, причём если было условие, то гарды выполнялись недетерменированно.
  • Хоар, 1978 описал CSP --- взаимодействующие последовательно процессы, это позволило доказывать корректность распределенных программ

[править] Развитие методов

  • Пнуэли, 1977 --- темпоральная логика, LTL. Стало возможным описывать свойства подмножеством языка и выполнимость словами языка (?)
  • Пнуэли, 1981 --- предложена логика ветвящегося времени, которая лучше подходит для тонких свойств параллельных программ
  • Клар, Эмерсон, 1981 --- предложен model checking, когда представляет программу в виде автомата с конечным числом состояний, обходим достижимые состояния и проверяем свойства.
  • Варди и Вольпер, 1986 -- анализ конформности в model checking, это снимает ограничение на конечность числа состояний.

В основном курсе будет уделять ся первому моделчекингу

  • Хольцман, 1989. Построен верификатор Spin

[править] Проблема комбинаторного взрыва

  • Бриан, 1989. Двоичные решающие диаграммы (BDD) --- мы строим пространство состояний, и склеиваем ветви согласно ряду правил
  • МакМиллан, 1993. Верификатор SMV, использующий BDD
  • Хольцман, Пелед, 1994 --- верификация параллельных систем.. Довольно часто бывает так, что порядок обмена не важен, тогда можно рассмотреть один из возможных --- редукция част. порядков
  • 1995. Редукция част. порядков в Spin

После этого стало возможным применять верификаторы в промышленности.

[править] Дальнейшее развитие

Было направлено на решение задачи комбинаторного взрыва

  • Кларк, 1992 --- абстракция для уменьшения модели
  • Эльсаиди, 1994 --- семантическая минимизация
  • Пелед, 1996 Бир, 1998 --- верификация на лету, подгрузка по мере анализа и удаление просмотренного куска дерева из памяти
  • Расси, 2000 - анализ достижимости с учётом спецификации --- выбор эвристики на основании свойств
  • Эмерсон и Прасад, 1994 --- симметрия

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

  • Сетевые и криптографические протоколы
  • Протоколы работы кэш-памяти
  • Интегральные схемы
  • Стандарты
  • Встроенные системы
  • Драйвера
  • Вообще программы на С. Для Spin есть конвертер из C в его внутренний язык


Верификация программ на моделях


01 02 03 04 05 06 07 08 09 10


Календарь

пт пт пт пт пт
Февраль
  08 15 22 29
Март
  14 21 28
Апрель
04 11 18

Материалы по курсу
Список вопросов к экзамену | Примеры задач: 1 2 3 4 5 | Теормин


Эта статья является конспектом лекции.

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Личные инструменты
Разделы