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

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

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.

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

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

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

Рефераты по инструментам верификации должны содержать следующее: предназначение, логика спецификаций, язык моделирования, возможности анализа ошибок, системные требования, примеры реальных программных систем, верифицированных с их помощью.

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

Список литературы

  1. Кулямин В.В. Методы верификации программного обеспечения - М.: Институт Системного Программирования РАН, 2008. – 111 с.
  2. Буздалов Д., Корныхин Е., Панфёров А. и др. Практикум по дедуктивной верификации программ — Издательский отдел факультета ВМиК МГУ им. М.В. Ломоносова; МАКС Пресс Москва, 2014. — С. 97.
  3. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. Издательство: БХВ-Петербург, 2010, 551 с.
  4. Эдмунд М. Кларк, мл., Орна Грамберг, Дорон Пелед Верификация моделей программ: Model Checking. Издательство Московского центра непрерывного математического образования Москва 2002. 416 с.
  5. http://www.cs.cmu.edu/~model check/s mv .html
  6. http://spinroot.com/spin/whatis pin.htm l
  7. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. – Москва, Радио и связь, 1988, 256с.

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

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


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

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