Содержание
- 2. Учебный план Лекции 12 часов: - Моделирование программ и систем, введение в SPIN - Спецификация проверяемых
- 3. Работа, баллы и оценки Практическая работа и индивидуальное задание 60 баллов - учебные задания из документации
- 4. Темы докладов Алгоритм Model Checking для CTL, пример Алгоритм Model Checking для LTL, пример Бинарные решающие
- 5. Источники Spin Model Checker manual and examples. URL: http://spinroot.com/spin/Man Ю.Г. Карпов. Model Checking. Верификация параллельных и
- 6. Model Checking Clarke & Emerson 1981: “Model checking is an automated technique that, given a finite-state
- 7. Принципы Model Checking 1. Для заданной вычислительной системы (программы или проекта микроэлектронной схемы) построить модель M
- 8. Model Checking Темпоральные логики позволяют описывать порядок событий во времени: CTL (Computational Tree Logic, ветвящаяся структура
- 9. Saul Aaron Kripke Родился 13 ноября 1940 г. Американский философ и логик Семантика Крипке для модальной
- 10. Модель Крипке Рассмотрим множество атомарных высказываний AP. Моделью Крипке M над множеством AP назовем четверку M
- 11. Пример (Волк, Коза, Капуста, Лодочник) AP ={ЛодочникСлева, КозаЖива, КапустаЦела} So = (←, ←, ←, ←) S
- 12. Пример Рассмотрим программу с переменными x, y ∈ D, D = {0, 1}. Программа содержит один
- 13. Пример Программа будет охарактеризована двумя формулами первого порядка: So(x, y ) ≡ x = 1 &
- 14. Модель Крипке на практике Степень детализации (сразу ли умрет коза) Параллельное исполнение (синхронное и асинхронное, взаимодействие
- 16. Скачать презентацию