Редактирование: ВПнМ, 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:
Задача верификации программ в общем случае алгоритмически неразрешима. Таким образом, применение формальных методов, несмотря на общее мнение, что там что-то доказывается, что невозможно, там приводится обоснование, что их нет.
Задача верификации программ в общем случае алгоритмически неразрешима. Таким образом, применение формальных методов, несмотря на общее мнение, что там что-то доказывается, что невозможно, там приводится обоснование, что их нет.
-
В абсолютном большинстве встречающиеся в природе системы таковы, что их ошибочность можно доказать, и это признак хорошего дизайна. По английcки это называется probably correct.
+
В абсолютном большщинстве встречающихся в природе системы таковы, что их ошибочность можно доказать, и это признак хорошего дизайна. По англицки это называется probably correct.
-
== Формальные методы ==
+
== Формлаьные методы ==
-
ФМ — использование математического аппарата, реализованного в языках, методах и средствах спецификации и верификации программ.
+
ФМ --- использование матаппарата, реализованного в языкамх, методах и средствах спец. и вериф. программ.
* Методы формальной спецификации
* Методы формальной спецификации
-
* Верификация
+
* Вериф
-
** Доказательство теорем
+
** Докю теорем
-
** Верификация на моделях
+
** Вериф. на моделях
== Методы верификации ==
== Методы верификации ==
-
* Полное тестирование. Тестирование, в ходе которого при построении тестового набора приводится обоснование, что набор полный.
+
* Полное тестирование. Тестирование, в ходе которого при постр. тестового набора приводится обосн., что набор оплный.
-
* Имитационное тестирование. Это то же тестирование, только оно помогает избежать в том случае, например, если система ещё не готова.
+
* Имитационное тестирование. Это то же тестирование, только оно помогает избежать в том случае, например, если симстема ещё не готова.
-
* Доказательство теорем
+
* Док. теорем
* Статический анализ
* Статический анализ
* Верификация на моделях
* Верификация на моделях
=== Тестирование ===
=== Тестирование ===
-
Грубо разделим эти методы на методы чёрного ящика, которые основываются на полном покрытии входных данных, и метод прозрачного ящика,который основывается на полном покрытии кода.
+
Грубо разделим эти методы на метод чёрного ящика, которые основываются на полном покрытии входных данных, метод прозрачного ящика основывается на полном покрытии кода.
Плюсы:
Плюсы:
* Проверяется та программа, которая будет использоваться
* Проверяется та программа, которая будет использоваться
-
* Для проведения теста не требуется дополнительных инструментальных средств
+
* Для проведения теста не требуется дополнительных интсрументальных средств
-
* Удобная локализация ошибки. Средства тестирования и отладки очень хорошо позволяют найти место в коде, где она находится
+
* Удобная локализация ошибки. Средства тетстирования и отладки очень хорошо позволяют найти место в коде, где она находится
Минусы:
Минусы:
* Не всегда есть условия для тестирования системы
* Не всегда есть условия для тестирования системы
-
* Проблема с воспроизводимостью тестов. Ошибка должна быть воспроизводима для понимания и отладки. Если речь идёт про системы взаимодействия с реальным окружением или когда она связана с историей взаимодействия, то в этих случаях ошибка может быть не воспроизводима.
+
* Проблема с воспроизводимостью тестов. Ошибка должна быть воспроизводима для понимания и отладки. Если речь идёт про системы взаимод. с реальным окружением, в этом случае она может быть невоспроизводима, или когда она связана с историей взаимодействия
Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д.
Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д.
-
Обоснование полноты тестового покрытия:
+
Обоснование оплноты тстового покрытия:
* ЧЯ: для последовательных программ сложно перебрать все входные данные
* ЧЯ: для последовательных программ сложно перебрать все входные данные
-
* ЧЯ: для параллельных дополнительно возникают цепочки взаимодействия и перестановки
+
* ЧЯ: для параллельных дополнительно возникают цепочки взаимод. и перестановки
-
* ЧЯ: для динамических структур, взаимодействующих с окружением --- невозможно
+
* ЧЯ: для динамических структур, взаимод. с окружением --- невозможно
-
* ПЯ: большой размер покрытия, растёт экспоненциально с размером
+
* ПЯ: большой размер покрытия, растёт жкспоненциально с размером
-
* Часто невозможно построение 100% покрытия, например, в случае наличия недостижимого кода.
+
* Часто невозможно постр. 100% покрытик
-
* Полное покрытие не гарантирует отсутствие ошибок.
+
* Полное покрытие не гарантирует отсут. ошибков.
Пример: полное покрытие для ЧЯ:
Пример: полное покрытие для ЧЯ:
-
* Поиск выигрышной стратегии в шашках — 10<sup>14</sup> операций (?)
+
* Поиск выигрышной стратегии в шашках --- 10^14 операций (?)
-
Пример невозможности построения полного покрытия для прозрачного ящика:
+
полное покрытие для прозрачного ящика:
-
int x = 1;
+
* //пример с ифами
-
if (x == 1) {
+
-
std::cout << "Okay" << std::endl;
+
-
} else {
+
-
std::cout << "Error" << std::endl;
+
-
}
+
-
Для этой программы нельзя построить полное покрытие — ветвь else ни при каких условиях не выполнится.
+
-
Полное тестовое покрытие — не панацея. Пусть у нас имеется функция с двумя ошибками:
+
Для программы 1 нельзя построить полное покрытие
-
int strlen(const char * p) {
+
 
-
int len = 0;
+
Для второй программы с двумя ошибками можно построить покрытие a, bbb, но оно не найдёт ни одну из них.
-
do {
+
-
++len;
+
-
} while (*p++);
+
-
return len;
+
-
}
+
-
Для неё можно построить покрытие "a", "bbb", но оно не выявит ни одну из ошибок.
+
Итоги:
Итоги:
-
* Полный перебор входных данных — невозможен
+
* Полный перебор вх. данных --- невозможен
-
* Полнота покрытия кода не гарантирует правильности
+
* Полноа покрытия кода не гарантирует правильности
-
<!-- Кто помнит, к чему это? --- !! Полнота вычислений -->
+
!! Полнота вычислений
==== Реактивные программы ====
==== Реактивные программы ====
-
Кроме традиционных программ, которые завершаются по окончании работы, описываются в терминах «вход/выход» и число состояний которых зависит только от входных данных и переменных, также существуют так называемые реактивные программы.
+
Эти программы работают в бесконечном цикле и взаимод. с окружении. Эти программы работают в терминах стимул/реакция. Здесь и возникает цепочка взаимод, которая резко увеличивает сост. системы, и обойти их тестированием не предст. возможным.
-
Эти программы работают в бесконечном цикле и взаимодействуют с окружением. Эти программы работают в терминах стимул/реакция. Здесь и возникает цепочка взаимодействия, которая резко увеличивает количество состояний системы, и обойти их тестированием не представляется возможным.
+
Реакт. программы это не пыльный ... на задворках программистких технологий, и ошбики там гораздо менее очевидны. Пример --- системы с разделением ресурсов.
-
Реактивные программы это не пыльный ... на задворках программистких технологий, и ошибки там гораздо менее очевидны. Пример — системы с разделением ресурсов.
+
== Системы с разделением ресурсов ==
-
 
+
* Дорожный траффик. Пример с дедлоком на перекрёстке
-
==== Системы с разделением ресурсов ====
+
-
* Дорожный трафик. Пример с дедлоком на перекрёстке
+
* Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка.
* Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка.
* ОС. Пример с дедлоком
* ОС. Пример с дедлоком
* ...
* ...
-
==== Параллельные системы ====
+
== Параллельные системы ==
Новый источник ошибок --- совместная работа проверенных компонентов.
Новый источник ошибок --- совместная работа проверенных компонентов.
-
Обычно считается, что программы надо строить из небольших компонент. Потом их интегрируем и всё работает. Однако, возникают ошбки на другом уровне: в 1993 году аэробус садился на мокрую полосу, нужно было включить реверс, но он включился поздно, потому что для его включения нужно, чтобы крутились колёса,были выпущены шасси и было давление на колёса, что случилось не сразу.
+
Обычно считается, что программы надо строить из небольших компонент. Потом их интегрируем и всё работает. Однако, возникают ошбки на другом уровне: в 1993 году аэробус садился на мокрую полосу, нужно было включить реверс, но он включился поздно, потому что для его включения нужно, чтобы крутились колёса, выпущены шасси и есть давление на колёса, что случилось не сразу.
Дополнительную сложность вносит одновременная работа.
Дополнительную сложность вносит одновременная работа.
-
=== Доказательство теорем ===
+
== Доказательство теорем ==
-
Есть система, свойства, есть аксиомы и правила вывода, и с помощью последних доказываются свойства.
+
Есть система, свойства, есть аксиомы иправила вывода, и с помощью последних доказываются свойства.
-
 
+
-
Пример:
+
-
Пусть у нас имеется система:
+
Фото 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, и выдвинул гипотезу, что если у нас для некоторого ЯП описаны assertions, то, с учётом того, как влияет оно на выполнение, можно доказать, что программа корректна
+
* Флойд, 1967. Ф. предложил использовать assertions, и выдвитнул гипотезу, что если у нас для некоторого ЯП описаны ass., то, с учётом того, как влияет оно на вып., можно доказать, что программа корректна
-
* Хоар ввёл триплеты (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, это снимает огр. на конеч. число сост.
В основном курсе будет уделять ся первому моделчекингу
В основном курсе будет уделять ся первому моделчекингу
-
* Хольцман, 1989. Построен верификатор Spin
+
* Хольцман, 1981. Построен верификатор 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 --- симметрия
-
== Области применения верификации на моделях ==
+
== Области применения вериф. на моделях ==
-
* Сетевые и криптографические протоколы
+
* Сетевые и криптограф. протоколы
* Протоколы работы кэш-памяти
* Протоколы работы кэш-памяти
-
* Интегральные схемы
+
* Инт. схемы
* Стандарты
* Стандарты
* Встроенные системы
* Встроенные системы
* Драйвера
* Драйвера
-
* Вообще программы на С. Для Spin есть конвертер из C в его внутренний язык
+
* Вообще программы на С. Для Spic есть конвертер из C в его внутр. язык
{{ВПнМ}}
{{ВПнМ}}
{{Lection-stub}}
{{Lection-stub}}

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!


Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.name/wiki/%D0%92%D0%9F%D0%BD%D0%9C%2C_01_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_08_%D1%84%D0%B5%D0%B2%D1%80%D0%B0%D0%BB%D1%8F%29
Личные инструменты
Разделы