Министерство образования и науки Российской Федерации Сибирский федеральный университет Магистратура
МЕТОДЫ ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ ПРОГРАММ Учебно-методическое пособие для самостоятельной работы Электронное издание
Красноярск СФУ 2013
УДК 004.42(07) ББК 32.973.2-018я73 М545
Составитель: Удалова Юлия Васильевна М545 Методы формальной верификации программ: учеб.-метод. пособие для самост. работы [Электронный ресурс] / сост. Ю.В. Удалова. – Электрон. дан. – Красноярск: Сиб. федер. ун-т, 2013. – Систем. требования: PC не ниже класса Pentium I; 128 Mb RAM; Windows 98/XP/7; Adobe Reader V8.0 и выше. – Загл. с экрана. Учебно-методическое пособие содержит указания по изучению теории, ознакомлению с современными автоматическими верификаторами и выполнению лабораторных работ учебного курса «Методы формальной верификации программ». Предназначено для направления 230100.68 «Информатика и вычислительная техника». УДК 004.42(07) ББК 32.973.2-018я73 © Сибирский федеральный университет, 2013
Учебное издание
Подготовлено к публикации ИЦ БИК СФУ Подписано в свет 08.02.2013 г. Заказ 155. Тиражируется на машиночитаемых носителях. Издательский центр Библиотечно-издательского комплекса Сибирского федерального университета 660041, г. Красноярск, пр. Свободный, 79 Тел/факс (391)206-21-49. E-mail
[email protected] http://rio.sfu-kras.ru
2
Оглавление Цели и задачи изучения дисциплины …………………………………………………4 Объем дисциплины и виды учебной работы ……………………………………........5 Получение навыков работы с автоматическим верификатором …. ………………...6 Указания для подготовки к лабораторным работам ………………. ………………...8 Указания к изучению теоретического курса ……………………… ………………...9 Библиографический список…………………………………………………………...10
3
Цели и задачи изучения дисциплины Изучение методов формальной верификации последовательных, многопоточных, многопроцессных и асинхронных программ предоставляет в распоряжение обучаемого набор теоретических и практических методов, позволяющих осуществлять проверку корректности различных программ на заданном множестве входных данных или на множестве возможных вычислений программы. Теоретические и практические знания методов формальной верификации позволяют проверять и корректировать как готовые программы, так и разрабатываемые алгоритмы. Такие знания и возможности способны значительно повысить надежность разрабатываемых программ. В результате изучения дисциплины студент должен знать: - этапы разработки программного обеспечения и место процесса верификации среди этих этапов; - примеры существующих автоматических программ-верификаторов и принципы их работы; - темпоральные логики CTL, LTL и принципы их применения для спецификации программы; - понятие модели программы и структуры для построения модели; - методы проверки на модели. Студент должен уметь: - строить модели программ и алгоритмов; - составлять спецификацию для программ и алгоритмов, используя темпоральные логики; - пользоваться возможностями автоматических верификаторов; - применять методы проверки на модели для верификации программ и алгоритмов; - составлять контрпримеры для ошибочных программ. Студент должен владеть: - методами построения моделей; - методами проверки на модели; - методами спецификации программ; - навыками работы с автоматическими верификаторами; - навыками повышения надежности разрабатываемых алгоритмов.
4
Объем дисциплины и виды учебной работы Аудиторные занятия – 36 часов: - лекции – 18 часов; - лабораторные работы – 18 часов. Самостоятельная работа: - изучение теоретического курса; - получение навыков работы с автоматическим верификатором; - подготовка к лабораторным работам.
5
Получение навыков работы с автоматическим верификатором Для изучения принципов работы современных автоматических верификаторов (в дополнении к верификатору Spin, используемому в курсе лабораторных работ) рекомендуются следующие программы и источники: 1. Верификатор Isabelle, используемые языки HOL, ML, поддерживается ОС Unix, информационные ресурсы: http://www.cl.cam.ac.uk/research /hvg/Isabelle/ index.html 2. Верификатор PVS, используемые языки HOL, Prolog, поддерживается ОС Unix, информационные ресурсы: http://pvs.csl.sri.com 3. Верификатор VCC, используемые языки C, поддерживается ОС Windows, информационные ресурсы: http://vcc.codeplex.com 4. Верификатор Bogor, используемые языки BIR, Java, поддерживается ОС Windows, информационные ресурсы: http://bogor.projects.cis.ksu.edu В рамках самостоятельной работы необходимо выбрать один из указанных верификаторов (или самостоятельно найти другой автоматический верификатор, обговорив целесообразность его изучения с преподавателем), изучить работу с ним и составить отчет, включающий следующие пункты. 1. Введение Краткое описание особенностей системы верификации. 2. Язык описания программ/моделей программ системы верификации Характеристика языка: ориентация на описание императивных, функциональных, объектно-ориентированных, асинхронных, многопоточных, многопроцессных программ. Если верификатор использует специальный язык верификации, например Promela или BIR, описать основы синтаксиса языка, поддерживаемые типы данных, функции и операторы. Если верификатор основан на стандартном языке программирования, как например С или Java, необходимо описать какое подмножество конструкций из этого языка он способен обрабатывать. 3. Примеры программ на языке системы верификации (пункт включается в отчет, только если верификатор использует специальный язык верификации) В примеры включить (если это возможно записать посредством языка выбранного верификатора): алгоритм с командой ветвления; циклический алгоритм; рекурсивный алгоритм; многопоточную программу; многопоточную программу с синхронизацией или защитой критической секции;
6
многопроцессную программу; многопроцессную программу с синхронизацией; многопроцессную программу с передачей сообщений; асинхронную программу. 4. Свойства, исследуемые системой верификации Указать, какие именно возможности проверки предоставляет верификатор, это может быть подтверждение спецификации пользователя, отслеживание функций asset и assume, исследование свойства завершимости программы, отслеживание критических секций, переполнения типов или операций выделения/освобождения памяти. 5. Язык описания спецификации программы (если спецификация поддерживается верификатором) Язык спецификации может поддерживать арифметические и логические выражения, темпоральные логики CTL или LTL, специальные функции для спецификации. 6. Примеры спецификации программ в системе верификации (если спецификация поддерживается верификатором) Удобно прописать спецификации к уже готовым примерам из пункта 3. 7. Интерфейс системы верификации Описание возможностей интерфейса, скриншоты, руководство пользователя, если поддерживается верификатором - возможности отладки, исследования контрпримера и т.п. 8. Примеры верификации программ Удобно описать процесс прохождения верификации и указать ее результаты для программ из пункта 3 и спецификаций из пункта 6. Если верификатор не поддерживает спецификацию пользователя, указать результаты исследования тех свойств программы, которые реализует выбранный верификатор. Обязательно привести пример верификации программы, содержащей ошибки.
7
Указания для подготовки к лабораторным работам Для выполнения лабораторных работ требуется вычислительная машина с установленным верификатором Spin (возможно скачивание с электронного ресурса http://spinroot.com). Выполнение лабораторных работ производится в компьютерных кассах на практических занятиях и в рамках самостоятельной работы. Желательна самостоятельная инсталляция верификатора Spin студентами на вычислительные машины, находящиеся в их личном пользовании. Для подготовки к лабораторным работам, изучения заданий лабораторных работ, примеров их выполнения и рекомендаций к построению программ и спецификаций используется учебное издание «Методы формальной верификации программ: учебно-методическое пособие по циклу лабораторных работ, Красноярск, 2013». Самостоятельно производится составление отчетов по выполненным лабораторным работам. При составлении отчетов ко всем лабораторным работам в соответствии с принятым стандартом оформляется титульный лист отчета, а также указываются цель работы, постановка задания, код программы, спецификация программы, словесное описание программы и спецификации, результаты верификации программы.
8
Указания к изучению теоретического курса Для самостоятельного изучения теории в дополнении к курсу лекций рекомендуется рассмотрение следующих тем из источника - Карпов Ю.Г. MODEL CHECKING. Верификация параллельных и распределенных программных систем (дополнительно рекомендуется источник - Кларк Э.М. Верификация моделей программ): - структура Крипке; - темпоральная логика CTL; - темпоральная логика LTL; - проверка модели для CTL; - проверка модели для LTL; - автомат Бюхи; - модели реагирующих систем; - спецификация реагирующих систем; - спецификация свойств достижимости, безопасности и справедливости. Дополнительно рекомендуется ознакомление с методами верификации, называемыми методами доказательства теорем, по источникам Лисков Б. Использование абстракций и спецификаций при разработке программ и Грис Д. Наука программирования. Стоит обратить особое внимание на следующие методы: - метод индуктивных утверждений; - метод индукции; - инварианты; - функции декремента.
9
Библиографический список Основной: 1. Карпов, Ю. Г. MODEL CHECKING. Верификация параллельных и распределенных программных систем / Ю. Г. Карпов. – СПб. : БХВ-Петербург, 2010. – 560 с. Дополнительный: 1. Кларк, Э. М. Верификация моделей программ / Э. М. Кларк, О. Грамберг, Д. Пелед. – М. : МЦНМО, 2002. – 416 с. 2. Лисков, Б. Использование абстракций и спецификаций при разработке программ / Б. Лисков, Дж. Гатэг. – М. : Мир, 1989. – 424 с. 3. Грис Д. Наука программирования / Д. Грис. – М. : Мир, 1984. – 416 с. Информационные ресурсы: 1. Верификатор Spin [Электронный ресурс]. – Режим доступа: http://spinroot.com. 2. Верификатор Bogor [Электронный ресурс]. – Режим доступа: http://bogor.projects.cis.ksu.edu. 3. Кулямин, В. В. Методы верификации программного обеспечения [Электронный ресурс] / В. В. Кулямин // Режим доступа: http://window.edu.ru/window_catalog/pdf2txt?p_id=27131. 4. Верификатор PVS [Электронный ресурс]. – Режим доступа: http://pvs.csl.sri.com. 5. Верификатор Isabelle [Электронный ресурс]. – Режим доступа: http://www.cl.cam.ac.uk/research/hvg/Isabelle. – Загл. с экрана. 6. Язык спецификации HOL [Электронный ресурс]. – Режим доступа: http://www.cl.cam.ac.uk/research/hvg/HOL. – Загл. с экрана.
10