ВПнМ/Теормин

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

Содержание 1 Лекция 1 2 Моделирование и абстракция 2.1 Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели. 2.2 Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе. 2.3 Моделирование программ. Графы программ. Статическая и операционная семантика. 2.4 Параллелизм. Чередование систем переходов. 2.5 Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными. 2.6 Параллелизм. Синхронный параллелизм. Рандеву. 2.7 Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. 2.8 Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели. 2.9 Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. 2.10 Абстракция. Абстракция графов программ. Отношение слабой симуляции.

Лекция 1

Валидация - исследование и обоснование того, что спецификация ПО и само ПО через реализованную в нём функциональность удовлетворяет ребованиям пользователей.

Верификация - исследование и обоснование того, что программа соответствует своей спецификации.

Верификация в общем случае алгоритмически неразрешима.

Методы верификации:

• "Полное" тестирование (слайды 14-22)
• Имитационное моделирование
• Доказательство теорем (27-29)
• Статический анализ (30-33)
• Верификация на моделях (34-38)

Моделирование и абстракция

Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели.

Схема верификации на моделях (Лекция 2, слайд 3)

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

Модель - упрощённое описание реальности, выполненное с определенной целью.

• с каждым объектом может быть связано несколько моделей
• каждая модель отражает свой аспект реальности

Аспекты модели:

• простота - модель должна быть проще, чем реальность
• корректность - не расходиться с реальностью
• адекватность - соответствовать решаемой задаче

Построение модели

1. формализация требований (постановка задачи моделирования)
2. выбор языка моделирования
3. абстракция системы до модели с учётом требований

Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.

Моделирование программ. Графы программ. Статическая и операционная семантика.

Параллелизм. Чередование систем переходов.

Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными.

Параллелизм. Синхронный параллелизм. Рандеву.

Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика.

Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели.

Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели.

Абстракция. Абстракция графов программ. Отношение слабой симуляции.