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

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

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. Концептуальные ошибки программного обеспечения (3- 4)
  2. Тестирование и формальная верификация: сравнение подходов (2- 3).
  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. Примеры использования инструментов доказательства теорем (2)
  14. Язык программирования Spec#
  15. Общие принципы устройства инструментов проверки моделей (2-3)
  16. Инструмент проверки моделей BLAST
  17. Инструмент проверки моделей SPIN
  18. Инструмент проверки моделей Java Pathfinder
  19. Инструмент проверки моделей NuSMV
  20. Инструмент проверки моделей Rabbit
  21. Инструмент проверки моделей Vereofy
  22. Инструмент проверки моделей UPPAAL
  23. Инструмент проверки моделей μCRL2
  24. Инструмент проверки моделей CPAchecker
  25. Доказательство теорем и проверка моделей: сравнение методов. (2- 3)
  26. Тьюринговские награды за работы в области формальной верификации.
  27. Примеры использования инструментов проверки моделей в промышленности (2-3)
  28. Примеры использования инструментов проверки моделей в космической отрасли (2-3)
  29. Примеры использования инструментов проверки моделей в телекоммуникациях (2-3)
  30. Примеры использования инструментов проверки моделей (2-3)
  31. Шаблоны спецификаций поведения систем. Качественные. Линейное время.
  32. Шаблоны спецификаций поведения систем. Качественные. Ветвящееся время.
  33. Шаблоны спецификаций поведения систем. Качественные. Реальное время.
  34. Шаблоны спецификаций поведения систем. Качественные. Вероятностные.
  35. Шаблоны спецификаций поведения систем. Составные события.
Длительность доклада по реферату составляет 10 минут и 3-5 минут отводится на вопросы.

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

Некоторые рефераты могут быть подготовлены совместно, либо по- отдельности, несколькими студентами. Темы таких рефератов дополнены количеством докладчиков в скобках. Каждый докладчик представляет свою часть реферата 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. http://patterns.projects.cs.ksu.edu/documentation/patterns.shtml
  8. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. – Москва, Радио и связь, 1988, 256с.
  9. Autili M., Grunske L., Lumpe M., Pelliccione P., Tang A. Aligning Qualitative, Real-Time, and Probabilistic Property Specification Patterns Using a Structured English Grammar // IEEE Transactions on Software Engineering, Volume: 41, Issue: 7, July 1 2015, pp. 620- 638.
  10. 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.
  11. Grunske L. Specification patterns for probabilistic quality properties // Proc. Of the 30th international conference on Software engineering. - ICSE '08. - New York, NY, USA: ACM, 2008. - Pp. 31-40.
  12. Konrad S., Cheng B. H. C. Real- time specification patterns // Proc. of the 27th International Conference on Software Engineering. ACM, 2005, pp. 372- 381.
  13. Mondragon O., Gates A. Q., Roach S. Prospec: Support for Elicitation and Formal Specification of Software Properties // Proc. of Runtime Verification Workshop, ENTCS, Vol. 89, Elsevier, 2004. pp. 67-88.
  14. Salamah S., Gates A. Q., Kreinovich V. Validated templates for specification of complex LTL formulas // J. of Syst. and Soft., 2012, V. 85, n. 8. pp. 1915- 1929.
  15. Post A., Menzel I., Podelski A. Applying restricted english grammar on automotive requirements: does it work? A case study // Proc. of 17th international working conference on Requirements engineering: foundation for software quality. Vol. 6606 of LNCS. Berlin, Heidelberg: Springer- Verlag, 2011. pp. 166-180.

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

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


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

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