Редактирование: ВПнМ, 01 лекция (от 08 февраля)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 231: | Строка 231: | ||
== История развития == | == История развития == | ||
- | * Флойд, 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, это снимает огр. на конеч. число сост. |
В основном курсе будет уделять ся первому моделчекингу | В основном курсе будет уделять ся первому моделчекингу | ||
* Хольцман, 1989. Построен верификатор Spin | * Хольцман, 1989. Построен верификатор 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 --- симметрия | ||