Новосибирский государственный университет

Факультет информационных технологий

ICT SBRAS
А.М.Федотов

Темы курса "Современные проблемы информатики"

Тема 05 : Проблемы верификации ПО

Контрольные вопросы:

1. Базовые понятия.
1.1. Постановка задачи. Надежность программ и систем.
1.2. Методы верификации
1.3. Логический язык спецификаций. Понятие корректности программ.
2. Методы дедуктивной верификации.
2.2. Метод индуктивных утверждений Флойда доказательства частичной корректности программ.
2.3. Метод фундированных множеств Флойда доказательства завершаемости программ.
2.4. Метод Хоара: частичная корректность программ, аксиоматическая семантика элементарных конструкций и циклов.
3. Проверка моделей.
3.1. Структура Крипке. Логическое представление программных систем.
3.2. Спецификация программных систем с помощью временных логик CTL и LTL.
3.3. Алгоритм проверки на модели формул временной логики CTL.
3.4. Алгоритм проверки на модели формул временной логики LTL.
3.5. Шаблоны спецификаций поведения систем.

Преподаватель: Наталья Олеговна Гаранина.

Темы рефератов:


1. Концептуальные ошибки программного обеспечения (2-3)
2. Тестирование и формальная верификация: сравнение подходов (2).
3. Принципы устройства инструментов автоматического доказательства теорем (2-3)
4. Инструмент автоматического доказательства теорем Coq
5. Инструмент автоматического доказательства теорем PVS
6. Инструмент автоматического доказательства теорем Vampire
7. Инструмент автоматического доказательства теорем Z3
8. Инструмент автоматического доказательства теорем Isabelle
9. Инструмент автоматического доказательства теорем E theorem prover
10. Примеры использования инструментов доказательства теорем в промышленности (2-3)
11. Примеры использования инструментов доказательства теорем в космической отрасли (2-3)
12. Примеры использования инструментов доказательства теорем в телекоммуникациях (2-3)
13. Примеры использования инструментов доказательства теорем, не вошедшие в п.10-12 (2)
14. Язык программирования Spec#
15. Принципы устройства инструментов проверки моделей (2-3)
16. Инструмент проверки моделей BLAST
17. Инструмент проверки моделей SPIN
18. Инструмент проверки моделей PRISM
19. Инструмент проверки моделей Java Pathfinder
20. Инструмент проверки моделей NuSMV
21. Инструмент проверки моделей UPPAAL
22. Инструмент проверки моделей μCRL2
23. Инструмент проверки моделей CPAchecker
24. Доказательство теорем и проверка моделей: сравнение методов. (2)
25. Тьюринговские награды за работы в области формальной верификации.
26. Примеры использования инструментов проверки моделей в промышленности (2- 3)
27. Примеры использования инструментов проверки моделей в космической отрасли (2-3)
28. Примеры использования инструментов проверки моделей в телекоммуникациях (2-3)
29. Примеры использования инструментов проверки моделей, не вошедшие в п.10- 12 (2)
30. Шаблоны спецификаций поведения систем. Линейное время.
31. Шаблоны спецификаций поведения систем. Ветвящееся время.

Длительность доклада по реферату каждого докладчика составляет 7 минут и 3-5 минут отводится на вопросы. Некоторые рефераты могут быть подготовлены совместно, либо по- отдельности, несколькими студентами. Темы таких рефератов дополнены количеством докладчиков в скобках.
Каждый докладчик представляет свою часть реферата 7 минут.

Указания для некоторых тем рефератов:
А) Рефераты по принципам устройства инструментов должны содержать следующее: сравнение нескольких инструментов, общее и отличие (см. п. B).
B) Рефераты по инструментам верификации должны содержать следующее: предназначение, логика спецификаций, язык моделирования, возможности анализа ошибок, системные требования, примеры реальных программных систем, верифицированных с их помощью.
C) Реферат по шаблонам спецификации должны содержать следующее: описание шаблонов 1) на естественном языке, 2) на языке какой-либо темпоральной логики, 3) графическое, а также примеры свойств систем.

Список литературы
1. Кулямин В.В. Методы верификации программного обеспечения - М.: Институт Системного Программирования РАН, 2008. – 111 с.
2. Д. Буздалов, Е. Корныхин, А. Панфёров и др. Практикум по дедуктивной верификации программ — Издательский отдел факультета ВМиК МГУ им. М.В. Ломоносова; МАКС Пресс Москва, 2014. — С. 97.
3. Ю.Г. Карпов Model Checking. Верификация параллельных и распределенных программных систем. Издательство: БХВ-Петербург, 2010, 551 с.
4. Эдмунд М. Кларк, мл., Орна Грамберг, Дорон Пелед. Верификация моделей программ: Model Checking. Издательство Московского центра непрерывного математического образования Москва 2002. 416 с.
5. http://www.cs.cmu.edu/~modelcheck/smv.html
6. http://spinroot.com/spin/whatispin.html
7. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. – Москва, Радио и связь, 1988, 256с.
8. Dwyer M. B., Avrunin G. S., Corbett J. C. Patterns in property specfications for finite-state verification // Proc. of the 21st Int. Conf. on Software Engineering, IEEE Computer Society Press, 1999, pp. 411-420. + сайт http://patterns.projects.cs.ksu.edu/documentation/patterns.shtml

Презентации по теме "Проблемы верификации ПО" :

Ссылка на презентацию.


|А.М.Федотов| |Преподавание| |Современные проблемы информатики| |Информатика| |Ключевые термины| |Персоны|

Федотов Анатолий Михайлович
[SBRAS]
НГУ
ФИТ НГУ
ИВТ СО РАН
© 2007-2018, Новосибирский государственный университет, Новосибирск
© 1998-2018, Институт вычислительных технологий СО РАН, Новосибирск
© 1998-2018, Федотов А.М.
    Дата последней модификации: 22.09.2018