6538
Науч. рук. Степанов Олег, к.т.н, СПбГУ ИТМО и JetBrains
- Главная
- Разное
- Дизайн
- Бизнес и предпринимательство
- Аналитика
- Образование
- Развлечения
- Красота и здоровье
- Финансы
- Государство
- Путешествия
- Спорт
- Недвижимость
- Армия
- Графика
- Культурология
- Еда и кулинария
- Лингвистика
- Английский язык
- Астрономия
- Алгебра
- Биология
- География
- Детские презентации
- Информатика
- История
- Литература
- Маркетинг
- Математика
- Медицина
- Менеджмент
- Музыка
- МХК
- Немецкий язык
- ОБЖ
- Обществознание
- Окружающий мир
- Педагогика
- Русский язык
- Технология
- Физика
- Философия
- Химия
- Шаблоны, картинки для презентаций
- Экология
- Экономика
- Юриспруденция
Применение шаблонов требований для формальной спецификации и верификации автоматных программ презентация
Содержание
- 1. Применение шаблонов требований для формальной спецификации и верификации автоматных программ
- 2. План Введение Шаблоны требований (ШТ) Применимость к автоматному программированию (АП) Запись требований Заключение
- 3. Проблема К АП хорошо применима верификация
- 4. Пример проблемы «Between the time an elevator
- 5. Существующее решение Графические нотации
- 6. Существующее решение (АП) Контракты: + Проще
- 7. Предлагаемое решение Записывать верифицируемые требования на подмножестве естественного языка
- 8. Детали Требования выводятся из грамматики Нет необходимости
- 9. Актуальность ШТ в контексте АП Васильева К.А.,
- 10. План Введение Шаблоны требований Применимость к АП Запись требований Заключение
- 11. Шаблоны требований ШТ – обобщенное описание (на
- 12. Шаблоны требований Требование = ШТ + Ограничение
- 13. Шаблоны требований Ограничение – та часть пути исполнения, на которой должно выполняться требование
- 14. Шаблоны требований
- 15. Шаблоны требований
- 16. Шаблон «Отсутствие»
- 17. План Введение Шаблоны требований Применимость ШТ к АП Запись требований Заключение
- 18. Анализ применимости Шаблоны были получены из требований
- 19. Пример организации результатов
- 20. Анализ применимости 118 требований к 15+
- 21. Оставшиеся 15% Ограниченность системы шаблонов
- 22. Оставшиеся 15% (Пример 1) Проблема в самой
- 23. Оставшиеся 15% (Пример 2) Особенности алгоритма преобразования?
- 24. Адаптация шаблонов к АП
- 25. План Введение Шаблоны требований Применимость к АП Запись требований Заключение
- 26. Грамматика (фрагмент) – стартовый нетерминальный символ
- 27. Методика вывода Неформальный алгоритм: Выделить свойство (требование)
- 28. Пример вывода (Оригинальное требование) «Система управления
- 29. Пример вывода (Шаг №1) «Система управления кофеваркой
- 30. Пример вывода (Шаг №2) Наречие «никогда»
- 31. Пример вывода (Шаг №3) →
- 32. Пример вывода (Шаг №4) Для любого
- 33. План Введение Шаблоны требований Применимость к АП Запись требований Заключение
- 34. Результаты Исследован вопрос применимости ШТ к спецификации
- 35. Дальнейшие исследования Теоретическая сторона: Анализ требований, которые
- 36. Конференции VII Межвузовская Конференция Молодых Ученых, СПбГУ
- 37. Спасибо! Вопросы? Клебанов Андрей, 6538
План Введение Шаблоны требований (ШТ) Применимость к автоматному программированию (АП) Запись требований Заключение
Слайд 1Применение шаблонов требований для формальной спецификации и верификации автоматных программ
Клебанов Андрей,
Слайд 2План
Введение
Шаблоны требований (ШТ)
Применимость к автоматному программированию (АП)
Запись требований
Заключение
Слайд 3Проблема
К АП хорошо применима верификация на модели
Однако работать с требованиями в
виде формул темпоральной логики трудоемко:
Сложно понять
Еще сложнее специфицировать корректно
Сложно понять
Еще сложнее специфицировать корректно
Слайд 4Пример проблемы
«Between the time an elevator is called at a floor
and the time it opens its doors at that floor, the elevator can arrive at that floor at most twice»
[]((call & <>open) ->
((!atfloor & !open) U
(open | ((atfloor & !open) U
(open | ((!atfloor & !open) U
(open | ((atfloor & !open) U
(open | (!atfloor U open))))))))))
Dwyer M. B., Avrunin G. S., Corbett J. C. Patterns in Property Specifications for Finite-state Verification / Proceedings of the 21st International Conference on Software Engineering. 1999
[]((call & <>open) ->
((!atfloor & !open) U
(open | ((atfloor & !open) U
(open | ((!atfloor & !open) U
(open | ((atfloor & !open) U
(open | (!atfloor U open))))))))))
Dwyer M. B., Avrunin G. S., Corbett J. C. Patterns in Property Specifications for Finite-state Verification / Proceedings of the 21st International Conference on Software Engineering. 1999
Слайд 5Существующее решение
Графические нотации
Облегчают восприятие, но не помогают при спецификации
Естественный язык
Слайд 6Существующее решение (АП)
Контракты:
+ Проще и понятней, чем темпоральные формулы
- Ограничены в
выразительных возможностях
- Трудоемко для нескольких состояний
Степанов О. Г. Методы реализации автоматных объектно-ориентированных программ. Диссертация на соискание ученой степени кандидата технических наук. СПбГУ ИТМО, 2009.
- Трудоемко для нескольких состояний
Степанов О. Г. Методы реализации автоматных объектно-ориентированных программ. Диссертация на соискание ученой степени кандидата технических наук. СПбГУ ИТМО, 2009.
Слайд 8Детали
Требования выводятся из грамматики
Нет необходимости в обработке естественного языка (NLP)
Гибкость для
разных предметных областей
Грамматика основывается на шаблонах требований (ШТ)
Для каждого требования существует формальная запись
Грамматика основывается на шаблонах требований (ШТ)
Для каждого требования существует формальная запись
Слайд 9Актуальность ШТ в контексте АП
Васильева К.А., Кузьмин Е.В. Верификация автоматных программ
с использованием LTL // Моделирование и анализ информационных систем. Ярославль: ЯрГУ. 2007. Т. 14, № 1, с. 3–14.
«… важным является вопрос о шаблонах (структуре) темпоральных свойств, наиболее применимых и адекватных для верификации автоматных программ. Наличие таких шаблонов позволяло бы говорить о классах темпоральных свойств автоматных моделей, что, несомненно, облегчало бы построение технологической схемы проверки автоматных программ на корректность относительно спецификации»
«… важным является вопрос о шаблонах (структуре) темпоральных свойств, наиболее применимых и адекватных для верификации автоматных программ. Наличие таких шаблонов позволяло бы говорить о классах темпоральных свойств автоматных моделей, что, несомненно, облегчало бы построение технологической схемы проверки автоматных программ на корректность относительно спецификации»
Слайд 11Шаблоны требований
ШТ – обобщенное описание (на формальном и естественном языках) часто
встречающихся ограничений на допустимые последовательности состояний в модели системы с конечным числом состояний
Формально описывают некий аспект поведения системы
Dwyer M. B., Avrunin G. S., Corbett J. C. Patterns in Property Specifications for Finite-state Verification / Proceedings of the 21st International Conference on Software Engineering. 1999
Формально описывают некий аспект поведения системы
Dwyer M. B., Avrunin G. S., Corbett J. C. Patterns in Property Specifications for Finite-state Verification / Proceedings of the 21st International Conference on Software Engineering. 1999
Слайд 13Шаблоны требований
Ограничение – та часть пути исполнения, на которой должно выполняться
требование
Слайд 14Шаблоны требований
Глобально
До Q
После Q
Между Q и R
После Q до R
Последовательность состояний
Q
R Q R Q
Ограничения
Слайд 18Анализ применимости
Шаблоны были получены из требований к обычным программам
Стоит ли использовать
шаблоны для специфицирования АП?
Т.е. можем ли выразить требования к АП, используя шаблоны, или у АП есть особенности?
Т.е. можем ли выразить требования к АП, используя шаблоны, или у АП есть особенности?
Слайд 20Анализ применимости
118 требований к 15+ программам из ~20 источников
85% покрывается 5
(из 8) шаблонами
Слайд 21Оставшиеся 15%
Ограниченность системы шаблонов
Проблема в самой модели
Особенности алгоритма преобразования исходной модели
в модель, пригодную для верификации
Слайд 22Оставшиеся 15% (Пример 1)
Проблема в самой модели?
ШТ «Отсутствие»:[](Q & !R ->
(!P W R))
Q: Ресурс заняли
P: Ресурс свободен
R: Ресурс освободили
Q: Ресурс заняли
P: Ресурс свободен
R: Ресурс освободили
Слайд 23Оставшиеся 15% (Пример 2)
Особенности алгоритма преобразования?
ШТ «Ответ» (на след. шаге): [](e1
-> X(z1))
e1
z1
e1
z1
Слайд 27Методика вывода
Неформальный алгоритм:
Выделить свойство (требование)
Выбрать шаблон и ограничение
Выполнить порождение
Использую данные шагов
№1 и №2 получить формальную запись для верификации
Слайд 28Пример вывода (Оригинальное требование)
«Система управления кофеваркой никогда не попадет в такое
состояние, в котором она не реагирует ни на события системного таймера, ни на нажатие кнопок «ОК» и «C»
Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и верификация «автоматных» программ // Программирование. 2008. № 1, c. 38–60.
Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и верификация «автоматных» программ // Программирование. 2008. № 1, c. 38–60.
Слайд 29Пример вывода (Шаг №1)
«Система управления кофеваркой никогда не попадет в такое
состояние, в котором она не реагирует ни на события системного таймера, ни на нажатие кнопок «ОК» и «C»
act = end
act = end
Слайд 30Пример вывода (Шаг №2)
Наречие «никогда» подсказывает, что должен быть использован шаблон
«Отсутствие» с ограничением «Глобально»
Слайд 31Пример вывода (Шаг №3)
→ → Для любого состояния
верно, что <шаблон> → Для любого состояния верно, что <отсутствие> → Для любого состояния верно, что никогда не выполняется P
Слайд 32Пример вывода (Шаг №4)
Для любого состояния верно, что никогда не выполняется
act = end
Формальный эквивалент для верификации:
AG!(act = end) и []!(act = end)
Формальный эквивалент для верификации:
AG!(act = end) и []!(act = end)
Слайд 34Результаты
Исследован вопрос применимости ШТ к спецификации АП
Проведена адаптация шаблонов
Разработаны грамматики для
записи требований на подмножестве русского и английского языков
Разработана методика записи верифицируемых требований
Разработана методика записи верифицируемых требований
Слайд 35Дальнейшие исследования
Теоретическая сторона:
Анализ требований, которые не удалось выразить (нет и в
оригинальной работе!)
Выделение новых шаблонов
Практическая сторона:
Wizard для формализации требования
Интеграция с инструментальным средством
Выделение новых шаблонов
Практическая сторона:
Wizard для формализации требования
Интеграция с инструментальным средством
Слайд 36Конференции
VII Межвузовская Конференция Молодых Ученых, СПбГУ ИТМО, 20-23.04.2010
Диплом за лучший доклад
на секции «Автоматное программирование»
Подана статья в «Научно-технический вестник СПбГУ ИТМО»
Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE 2010), Нижний Новгород, 1-2.06.2010
Workshop on Program Semantics, Specification and Verification: Theory and Applications (PSSV 2010) в рамках Computer Science Symposium in Russia (CSR 2010), Казань, 14-15.06.2010
Подана статья в «Научно-технический вестник СПбГУ ИТМО»
Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE 2010), Нижний Новгород, 1-2.06.2010
Workshop on Program Semantics, Specification and Verification: Theory and Applications (PSSV 2010) в рамках Computer Science Symposium in Russia (CSR 2010), Казань, 14-15.06.2010
