Применение шаблонов требований для формальной спецификации и верификации автоматных программ Клебанов Андрей, 6538 Науч. рук. Степанов Олег, к.т.н, СПбГУ. - презентация

1 Применение шаблонов требований для формальной спецификации и верификации автоматных программ Клебанов Андрей, 6538 Науч. рук. Степанов Олег, к.т.н, СПбГУ ИТМО и JetBrains

2 2 План Введение Шаблоны требований (ШТ) Применимость к автоматному программированию (АП) Запись требований Заключение

3 3 Проблема К АП хорошо применима верификация на модели Однако работать с требованиями в виде формул темпоральной логики трудоемко: –Сложно понять –Еще сложнее специфицировать корректно

4 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

5 5 Существующее решение Графические нотации Облегчают восприятие, но не помогают при спецификации Естественный язык

6 6 Существующее решение (АП) Контракты: + Проще и понятней, чем темпоральные формулы - Ограничены в выразительных возможностях - Трудоемко для нескольких состояний Степанов О. Г. Методы реализации автоматных объектно- ориентированных программ. Диссертация на соискание ученой степени кандидата технических наук. СПбГУ ИТМО, 2009.

7 7 Предлагаемое решение Записывать верифицируемые требования на подмножестве естественного языка

8 8 Детали Требования выводятся из грамматики Нет необходимости в обработке естественного языка (NLP) Гибкость для разных предметных областей Грамматика основывается на шаблонах требований (ШТ) Для каждого требования существует формальная запись

9 9 Актуальность ШТ в контексте АП Васильева К.А., Кузьмин Е.В. Верификация автоматных программ с использованием LTL // Моделирование и анализ информационных систем. Ярославль: ЯрГУ Т. 14, 1, с. 3–14. «… важным является вопрос о шаблонах (структуре) темпоральных свойств, наиболее применимых и адекватных для верификации автоматных программ. Наличие таких шаблонов позволяло бы говорить о классах темпоральных свойств автоматных моделей, что, несомненно, облегчало бы построение технологической схемы проверки автоматных программ на корректность относительно спецификации»

10 10 План Введение Шаблоны требований Применимость к АП Запись требований Заключение

11 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

12 12 Шаблоны требований Требование = ШТ + Ограничение

13 13 Шаблоны требований Ограничение – та часть пути исполнения, на которой должно выполняться требование

14 14 Шаблоны требований Глобально До Q После Q Между Q и R После Q до R Последовательность состояний Q R Q R Q Ограничения

15 15 Шаблоны требований Система шаблонов Наличие Порядок Отсутствие Ограниченное существование Всеобщность Существование Предшествование Ответ Цепное предшествование Цепной ответ

16 16 Шаблон «Отсутствие» ЦельИспользуется для описания части пути исполнения системы, в которой нет определенного состояния. Так же известен как «Никогда». ЗаписьLTLОграничениеЗапись Глобально [](!P) До RR -> (!P U R) После Q[](Q -> [](!P)) Между Q и R []((Q & !R & R) -> (!P U R)) После Q до R[](Q & !R -> (!P W R)) CTLОграничениеЗапись Глобально AG(!P) После QAG(Q -> AG(!P)) …… После Q до RAG(Q & !R -> A[!P W R]) Пример использования Этот шаблон может быть применен для описания общих свойств модели в целом или отдельной группы состояний. Для специфицирования свойства безопасности (safety) следует использовать это шаблон и ограничение «Глобально». Например, в том случае, когда необходимо выразить свойство вида: «Автомат A никогда не перейдет в состояние s », «В состоянии s никогда не будет обработано событие e » или свойство «Тупиковое состояние» из разд Связь с другими шаблонами …

17 17 План Введение Шаблоны требований Применимость ШТ к АП Запись требований Заключение

18 18 Анализ применимости Шаблоны были получены из требований к обычным программам Стоит ли использовать шаблоны для специфицирования АП? Т.е. можем ли выразить требования к АП, используя шаблоны, или у АП есть особенности?

19 19 Пример организации результатов ТребованиеИсходная формальна запись Шаблон, Ограничение Источник 9Система управления кофеваркой никогда не попадет в такое состояние, в котором она никак не реагирует ни на события системного таймера, ни на нажатие кнопок «ОК» и «C». !(EF act = end) Отс., Глобально AG(!P) !EF(P), P: act = end 5

20 20 Анализ применимости 118 требований к 15+ программам из ~20 источников 85% покрывается 5 (из 8) шаблонами

21 21 Оставшиеся 15% Ограниченность системы шаблонов Проблема в самой модели Особенности алгоритма преобразования исходной модели в модель, пригодную для верификации

22 22 Оставшиеся 15% (Пример 1) Проблема в самой модели? ШТ «Отсутствие» : [](Q & !R -> (!P W R)) Q: Ресурс заняли P: Ресурс свободен R: Ресурс освободили Если ресурс заняли, то он несвободен, пока его не освободят. o1.x1 W o1.z1 & G (o1.z2 -> (o1.x1 W o1.z1) & o1.z1 -> (!o1.x1 W o1.z2))

23 23 Оставшиеся 15% (Пример 2) Особенности алгоритма преобразования? ШТ «Ответ» (на след. шаге) : [](e 1 -> X(z 1 )) Непосредственно после открытия двери загорается лампочка. e 1 U z 1 e1e1 z1z1 e1e1 z1z1

24 24 Адаптация шаблонов к АП Пример использования Этот шаблон может быть применен для описания общих свойств модели в целом или отдельной группы состояний. Для специфицирования свойства безопасности (safety) следует использовать это шаблон и ограничение «Глобально». Например, в том случае, когда необходимо выразить свойство вида: «Автомат A никогда не перейдет в состояние s », «В состоянии s никогда не будет обработано событие e » или свойство «Тупиковое состояние» из разд Examples and Known Uses The most common example is mutual exclusion. In a state- based model, the scope would be global and P would be a state formula that is true if more than one process is in its critical section.

25 25 План Введение Шаблоны требований Применимость к АП Запись требований Заключение

26 26 Грамматика (фрагмент) ::= ::= «Для любого состояния верно, что» | «До состояния, в котором Q, верно что» | «После состояния, в котором Q, верно что» | «Между состоянием, в котором Q, до состояния, в котором R, верно что» | «После состояния, в котором Q, до состояния, в котором R, верно что» ::= | | | | | ::= «никогда не выполняется P » ::= «всегда выполняется P » ::= «когда-нибудь выполнится P » …… – стартовый нетерминальный символ

27 27 Методика вывода Неформальный алгоритм: 1.Выделить свойство (требование) 2.Выбрать шаблон и ограничение 3.Выполнить порождение 4.Использую данные шагов 1 и 2 получить формальную запись для верификации

28 28 Пример вывода (Оригинальное требование) «Система управления кофеваркой никогда не попадет в такое состояние, в котором она не реагирует ни на события системного таймера, ни на нажатие кнопок «ОК» и «C» Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и верификация «автоматных» программ // Программирование , c. 38–60.

29 29 Пример вывода (Шаг 1) «Система управления кофеваркой никогда не попадет в такое состояние, в котором она не реагирует ни на события системного таймера, ни на нажатие кнопок «ОК» и «C» act = end

30 30 Пример вывода (Шаг 2) Наречие «никогда» подсказывает, что должен быть использован шаблон «Отсутствие» с ограничением «Глобально»

31 31 Пример вывода (Шаг 3) Для любого состояния верно, что Для любого состояния верно, что Для любого состояния верно, что никогда не выполняется P

32 32 Пример вывода (Шаг 4) Для любого состояния верно, что никогда не выполняется act = end Формальный эквивалент для верификации: AG!(act = end) и []!(act = end)

33 33 План Введение Шаблоны требований Применимость к АП Запись требований Заключение

34 34 Результаты Исследован вопрос применимости ШТ к спецификации АП Проведена адаптация шаблонов Разработаны грамматики для записи требований на подмножестве русского и английского языков Разработана методика записи верифицируемых требований

35 35 Дальнейшие исследования Теоретическая сторона: –Анализ требований, которые не удалось выразить (нет и в оригинальной работе!) –Выделение новых шаблонов Практическая сторона: –Wizard для формализации требования –Интеграция с инструментальным средством

36 36 Конференции VII Межвузовская Конференция Молодых Ученых, СПбГУ ИТМО, Диплом за лучший доклад на секции «Автоматное программирование» Подана статья в «Научно-технический вестник СПбГУ ИТМО» Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE 2010), Нижний Новгород, Workshop on Program Semantics, Specification and Verification: Theory and Applications (PSSV 2010) в рамках Computer Science Symposium in Russia (CSR 2010), Казань,

37 37 Спасибо! Вопросы? Клебанов Андрей, 6538