Содержание

Слайд 2

Учебный план

Лекции 12 часов:
- Моделирование программ и систем, введение в SPIN
- Спецификация

Учебный план Лекции 12 часов: - Моделирование программ и систем, введение в
проверяемых свойств, LTL
- Разбор примеров верификации программ
- Разбор примеров верификации параллельных программ
- Обзор и сравнение программ для ModelChecking с примерами (NASA/JPL, SMV, Uppaal, Kronos)
- Алгоритмы верификации и оптимизации
Практика 26 часов
Домашняя работа 100+ часов

Слайд 3

Работа, баллы и оценки

Практическая работа и индивидуальное задание 60 баллов
- учебные задания

Работа, баллы и оценки Практическая работа и индивидуальное задание 60 баллов -
из документации SPIN 15
http://spinroot.com/spin/Man/Exercises.html
- индивидуальная задача на SPIN 15
- задачи на LTL15
- доклад 15
Экзамен письменно (?) 40 баллов
Пропущенная пара -2 балла
Оценка - Баллы
5 >= 90
4 >= 75
3 >= 60

Слайд 4

Темы докладов

Алгоритм Model Checking для CTL, пример
Алгоритм Model Checking для LTL, пример
Бинарные

Темы докладов Алгоритм Model Checking для CTL, пример Алгоритм Model Checking для
решающие диаграммы, свойства, операции, применение
Символьный алгоритм Model Checking для CTL, пример
Алгоритм Model Checking для PCTL, пример
Алгоритм Model Checking для TCTL, пример
SPIN optimization: partial order reduction
SPIN optimization: bitstate hashing
SPIN optimization: minimised automaton representation of reachable states
SPIN optimization: state vector compression
SPIN optimization: dataflow analysis and slicing algorithm
Обзор и сравнение программ для ModelChecking: NASA/JPL (для Java кода)
Обзор и сравнение программ для ModelChecking: SMV (символьный)
Обзор и сравнение программ для ModelChecking: Uppaal (в реальном времени)
Обзор и сравнение программ для ModelChecking: Kronos (в реальном времени)

Слайд 5

Источники

Spin Model Checker manual and examples.
URL: http://spinroot.com/spin/Man
Ю.Г. Карпов. Model Checking. Верификация параллельных

Источники Spin Model Checker manual and examples. URL: http://spinroot.com/spin/Man Ю.Г. Карпов. Model
и распределенных программ
При разработке программы использованы материалы:
Spin Workshops, Advanced Spin Tutorial, Theo C. Ruys & Gerard J. Holzmann
Курс «Верификация моделей программ», лектор Владимир Захаров
Курс «Верификация программ на моделях» лектор Константин Савенков
LTL Spec Patterns, SAnToS laboratory
Учебное пособие «Верификация программ методом Model Checking» А.М.Миронов
Concise Promela Reference, Rob Gerth
Книга «Верификация моделей программ», Кларк, Грамберг, Пелед
Курс «Logic Model Checking», CS118, Caltech, Gerard J. Holzmann

Слайд 6

Model Checking

Clarke & Emerson 1981:
“Model checking is an automated technique that, given

Model Checking Clarke & Emerson 1981: “Model checking is an automated technique
a finite-state model of a system and a logical property, systematically checks whether this property holds for (a given initial state in) that model.”

Слайд 7

Принципы Model Checking
1. Для заданной вычислительной системы (программы или
проекта микроэлектронной

Принципы Model Checking 1. Для заданной вычислительной системы (программы или проекта микроэлектронной
схемы) построить модель M
- дискретную структуру, которая
- может рассматриваться как интерпретация для некоторой
формальной логики, и
- описывает (на некотором уровне абстракции) поведение
вычислительной системы.
2. Для технических требований, предъявляемых к системе,
сформулировать эти требования на формальном
логическом языке задать спецификацию ϕ.
3. Проверить выполнимость спецификации ϕ на модели M:
M |= ϕ

Слайд 8

Model Checking

Темпоральные логики позволяют описывать порядок событий во времени:
CTL (Computational Tree Logic,

Model Checking Темпоральные логики позволяют описывать порядок событий во времени: CTL (Computational
ветвящаяся структура времени)
LTL (Linear Temporal Logic, линейная)
PCTL (Probabilistic, вероятностная)
TCTL (в реальном времени)
Cмысл всякой формулы темпоральной логики определяется по отношению к размеченному графу переходов.
Исторически структуры такого вида называются моделями Крипке (Kripke structure).
Задача model checking M |= ϕ

Слайд 9

Saul Aaron Kripke
Родился 13 ноября 1940 г.
Американский философ и логик
Семантика Крипке для

Saul Aaron Kripke Родился 13 ноября 1940 г. Американский философ и логик
модальной логики
Naming and Necessity (Prinston, 1972, 1980)

Слайд 10

Модель Крипке

Рассмотрим множество атомарных высказываний AP.
Моделью Крипке M над множеством AP назовем

Модель Крипке Рассмотрим множество атомарных высказываний AP. Моделью Крипке M над множеством
четверку
M = (S, S0 , R, L):
1) S — конечное множество состояний;
2) So ⊆ S — множество начальных состояний;
3) R ⊆ S × S — отношение переходов, которое обязано быть
тотальным, т. е. для каждого состояния s ∈ S должно
существовать такое состояние s ∈ S , что имеет место
R(s, s );
4) L : S → 2AP — функция разметки, которая помечает
каждое состояние множеством атомарных высказываний,
истинных в этом состоянии.

Слайд 11

Пример

(Волк, Коза, Капуста, Лодочник)
AP ={ЛодочникСлева, КозаЖива, КапустаЦела}
So = (←, ←, ←, ←)
S

Пример (Волк, Коза, Капуста, Лодочник) AP ={ЛодочникСлева, КозаЖива, КапустаЦела} So = (←,
= {(←, ←, ←, ←), (←, →, ←, →), (←, †, →, →), …}
R = {((←, ←, ←, ←), (←, →, ←, →)),
((←, ←, ←, ←), (←, †, →, →)), …}
L((←, ←, ←, ←)) = (ЛодочникСлева, КозаЖива, КапустаЦела)
L((←, †, →, →)) = (КапустаЦела)

Слайд 12

Пример

Рассмотрим программу с переменными
x, y ∈ D, D = {0, 1}.
Программа содержит

Пример Рассмотрим программу с переменными x, y ∈ D, D = {0,
один переход
x := (x + y)(mod2),
В начальном состоянии
x = 1 и y = 1.

Слайд 13

Пример

Программа будет охарактеризована двумя формулами первого порядка:
So(x, y ) ≡ x

Пример Программа будет охарактеризована двумя формулами первого порядка: So(x, y ) ≡
= 1 & y = 1,
R(x, y , x , y) ≡ x = (x + y )(mod2) & y = y.
Модель Крипке M = (S, S0 , R, L) такова:
S = D × D;
So = {(1, 1)};
R = {((1, 1), (0, 1)), ((0, 1), (1, 1)),
((1, 0), (1, 0)), ((0, 0), (0, 0))};
L((1, 1)) = {x = 1, y = 1}, L((0, 1)) = {x = 0, y = 1},
L((1, 0)) = {x = 1, y = 0}, L((0, 0)) = {x = 0, y = 0}.
Единственный путь в модели Крипке, исходящий из начального состояния, имеет вид (1, 1)(0, 1)(1, 1)(0, 1) . . .

Слайд 14

Модель Крипке на практике

Степень детализации (сразу ли умрет коза)
Параллельное исполнение (синхронное и

Модель Крипке на практике Степень детализации (сразу ли умрет коза) Параллельное исполнение
асинхронное, взаимодействие через общую память и сообщения)
Трансляция программ в модели Крипке (методы оптимизации по памяти)
Имя файла: Model-Checking.pptx
Количество просмотров: 192
Количество скачиваний: 0