Программа учебного курса
Формальные методы в программной инженерии
Курс предназначен для магистрантов Математического Факультета НГУ. Объем дисциплины _8 __зачетных единиц, в том числе в академических часах по видам учебных занятий:
Семестр | учебные занятия | форма промежуточной аттестации (зачет, дифференцированный зачет, экзамен) | |||||||
Общий объем | в том числе | ||||||||
контактная работа обучающихся с преподавателем | СРС | ||||||||
Всего | из них | ||||||||
Лекции | Лаборные занятия | Практи ческие занятия | КСР | Консультации | |||||
1 | 301 | 26 | 16 | 6 | 4 | 111 | экзамен | ||
2 | 44 | 24 | 12 | 8 | 120 | экзамен |
Лекторы: Чушкин Михаил Сергеевич
, к. т.н.
Шилов Николай Вячеславович, к. ф.-м. н.
Гаранина Наталья Олеговна, к. ф.-м. н.
Пономарев Денис Константинович, к. ф.-м. н.
Формальные методы (Formal methods) – направление в Computer Science, развиваемое более 40 лет. Ежегодно проводится более десятка международных конференций по различным аспектам формальных методов.
Обязательным базисом формальных методов являются формальные спецификации программ, баз данных, онтологий, требований в системотехнике и др. объектов. Формальные спецификации являются основой в разнообразных инструментах анализа и верификации различной силы от тестирования и статического анализа программ до дедуктивной верификации.
Курс состоит из четырех разделов, читаемых разными лекторами:
· спецификация и верификация моделей с помощью SMT-решателей
· спецификация и верификация программ в предикатном и автоматном программировании
· верификация программных систем методом проверки моделей (model checking)
· методы спецификации и анализа терминологических систем
Наряду с изложением теоретических основ в рамках курса предполагается интенсивное практическое освоение студентами методов формальной спецификации, а также различных инструментов верификации и анализа. В рамках каждого из четырех разделов курса предполагается проведение блока студенческих заданий, состоящего из двух частей:
· спецификация содержательно сформулированной простой задачи (онтологии) на языке соответствующего инструмента верификации;
· проведение верификации программы (анализа онтологии) относительно спецификации с применением соответствующего инструмента верификации.
Инструменты верификации и анализа, применяемые в студенческих заданиях: генератор формул корректности предикатных программ, система автоматического интерактивного доказательства PVS, SMT-решатели Yices и Z3, model checker Spin, редактор онтологий Protege, машины вывода ELK и Fact++.
Данный курс базируется на знании и умении по следующим дисциплинам: основам математической логики, теории графов, языкам программирования и методам трансляции.
I. Цели и задачи курса
Цель курса – сформировать у студентов убежденность в значимости формальной логики для решения прикладных задач программной инженерии. Курс направлен на изучение и освоение методов формальной спецификации, анализа, синтеза и верификации программ, моделей программ и онтологий.
Теоретический материал курса определяет необходимую основу для выполнения студентами практического индивидуальному задания по каждому разделу курса. Выполнению индивидуального задания предшествует проведение коллективных практических занятий по написанию формальных спецификаций для тестовых примеров с последующим разбором вариантов и методов спецификации, а также типичных ошибок.
Главной задачей курса является формирование у студентов устойчивого владения методами формальной спецификации со способностью применения этих методов для реально возникающих задач. Этому способствует наличие четырех блоков заданий различного вида на формальную спецификацию. Одним из показателей владения формальными методами станет степень формализации в выпускной магистерской диссертации студента.
2. Содержание дисциплины
Новизна и актуальность курса
Опыт проведения студенческих заданий на формальную спецификацию и дедуктивную верификацию имеется в рамках курса «Формальные методы в описании языков и систем программирования» на ФИТ НГУ. Задания на формальную спецификацию даются студентам с 2006г., а на дедуктивную верификацию – с 2012г. Следует отметить, что курс с заданиями на формальную спецификацию и дедуктивную верификацию существует только в МГУ на МВК уже 5-7 лет, причем уровень требований к студентам там существенно выше, чем в НГУ.
Структура курса
№ п/п | Раздел (тема) дисциплины | Семестр (из учебного плана) | Неделя семестра (из учебного плана) | Контактная работа обучающихся с преподавателем по видам учебных занятий (из учебного плана, в часах) | Самостоятельная работа обучающихся (из учебного плана, в часах) | Формы текущего контроля успеваемости (по неделям семестра) Форма промежуточной аттестации (по семестрам, из учебного плана) | ||||
лекции | Лабораторные занятия | Практические занятия | Контроль самостоятельной работы (КСР) | Консультации | ||||||
1 | SMT-решатели | 1 | 3-5 | 4 | 2 | 20 | устный опрос Задание на построение модели в Z3 | |||
2.1 | Основы предикатного программирования | 1 | 6-7 | 4 | 15 | устный опрос | ||||
2.2 | Методы предикатного программирования | 1 | 8-10 | 5 | 4 | 2 | 38 | устный опрос Задание на спецификацию. Задание на доказательство в PVS | ||
2.3 | Автоматное программирование | 1 | 10-11 | 3 | 22 | устный опрос | ||||
Итоговая аттестация | 1 | 16 | 2 | 16 | экзамен | |||||
3.1 | Метод проверки моделей: моделирование и спецификация систем | 2 | 1-2 | 4 | 2 | 6 | устный опрос Задание на логическое представление и спецификацию программных систем | |||
3.2 | Проверка моделей на практике: инструменты и типичные задачи | 2 | 3-4 | 4 | 2 | 2 | 30 | устный опрос Конторольные задания на верификацию в системах SPIN и SMV | ||
3.3 | Алгоритмы проверки моделей: классические и оптимизированные | 2 | 5-6 | 4 | 2 | 2 | 20 | устный опрос Задание на построение BDD | ||
4.1 | Моделирование терминологических систем на основе логических методов | 2 | 7-8 | 4 | 2 | 8 | Задание на формализацию терминологий Коллективная работа с системой Protégé | |||
4.2 | Методы автоматического доказательства в дескрипционных логиках | 2 | 9-10 | 4 | 2 | 2 | 16 | Задание на построение и анализ доказательств Контрольная работа | ||
4.3 | Анализ терминологических систем на основе логического вывода | 2 | 11-12 | 4 | 2 | 2 | 24 | Задание на анализ терминологий Коллективная работа с расширениями Protégé для анализа терминологий Контрольная работа | ||
Итоговая аттестация | 2 | 15 | 2 | 16 | экзамен | |||||
ИТОГО часов: |
Содержание отдельных разделов и тем
Раздел 1. SMT-решатели
1.1. Задача выполнимости булевых формул (Boolean satisfiability problem)
Необходимые основы математической логики. Задача SAT. Алгоритм Дэвиса-Патнема-Логемана-Лавленда (DPLL). Алгоритм управляемого конфликтами обучения дизъюнктам (CDCL).
1.2. Задача выполнимости формул в теориях (Satisfiability modulo theories)
Формулировка простейшей задачи SMT. Алгоритм решения задачи SMT через задачу SAT. Т – решатели. Алгоритмы решения: DPPL(T). Язык SMT-LIB. Решатели Yices и Z3.
Раздел 2. Спецификация и верификация программ в предикатном и автоматном программировании
2.1. Основы предикатного программирования
2.1.1. Теория программ-функций
Классификация программ. Класс программ-функций.
Программа со спецификацией в виде тройки Хоара. Однозначность и тотальность спецификации и программы.
Определение операционной семантики программы-функции.
Тотальная корректность программы.
Лемма о тотальности спецификации.
Теорема тождества спецификации и программы
Следствия теоремы тождества спецификации и программы
2.1.2. Математические основы
Отношения порядка. Основные положения теории наименьшей неподвижной точки. Методы математической индукции.
2.1.3. Язык вычислимых предикатов и его операционная семантика.
Язык вычислимых предикатов P0. Структура программы. Операторы, их предикатная и программная формы. Базисные предикаты. Полная программа. Функциональная форма.
Операционная семантика операторов языка P0.
Семантика рекурсивных предикатов. Рекурсивное кольцо предикатов. Система логических тождеств рекурсивного кольца. Лемма о непрерывности оператора суперпозиции, параллельного оператора и условного оператора относительно предикатов-семантик. Операционная семантика рекурсивного предиката.
Семантика полной программы. Лемма о тождестве операторов с их операционной семантикой. Теорема о тождестве программы на языке P0 и ее операционной семантики. Теорема однозначности программы.
Операционная семантика неоднозначных предикатов.
2.1.4. Построение языка предикатного программирования
Язык P1: подстановка программы на место вызова.
Язык P2: оператор суперпозиции и параллельный оператор общего вида. Оператор суперпозиции наиболее общего вида.
Язык P3: выражения. Функциональный и операторный стили.
Язык P4: типы, полный язык. Лексика. Структура предикатной программы. Основные операторы. Выражения. Описание переменных. Описание типов. Алгебраические типы. Списки. Массивы. Формулы.
Язык Pimp: императивное расширение языка предикатного программирования. Модифицируемые переменные.
2.2. Методы предикатного программирования
2.2.1. Оптимизирующие трансформации предикатной программы.
Подстановка определения предиката на место вызова. Групповой оператор присваивания и способ его раскрытия. Замена хвостовой рекурсии циклом. Склеивание переменных. Метод обобщения исходной задачи. Кодирование алгебраических типов. Методы кодирование списков через вырезки массива на примере программы суммирования элементов списка. Кодирование списка указателями в программе обращения списка.
Программа сортировки простыми вставками. Оптимизация алгоритма. Построение императивной программы.
2.2.2. Стили предикатного программирования.
Синтез программ с однозначной спецификацией. Синтез программ с произвольной спецификацией. Базисные формы декомпозиции программы. Традиционный стиль программирования. Применение дедуктивной верификации программ.
Гиперфункции. Проблемы реализации ветвления в программе. Определение гиперфункции и оператора продолжения ветвей. Определение предиката-гиперфункции. Спецификация предиката-гиперфункции. Синтаксические правила для оператора продолжения ветвей. Свойства гиперфункций. Построение программы «сумма чисел в строке». Использование гиперфункций в программе решения системы линейных уравнений.
2.2.3. Дедуктивная верификация предикатных программ
Структура правила доказательства корректности; посылки, следствие. Правила для формулы тотальной корректности и теоремы тождества спецификации и программы.
Правила декомпозиции доказательства для общего случая. Правила для параллельного оператора, условного оператора, оператора суперпозиции, оператора суперпозиции с корректным первым подоператором.
Декомпозиция вхождений операторов в формулах корректности.
Правила для корректных подоператоров.
Правила декомпозиции доказательства для случая однозначной спецификации.
Правила доказательства корректности для рекурсивно определяемого предиката.
Примеры доказательства корректности программ.
Система автоматизации доказательства PVS. Назначение, основные компоненты и принципы работы. Типы и описания языка спецификаций системы PVS. Формулы, теоремы и теории языка спецификаций системы PVS. Библиотеки теорий.
Блок доказательства (Prover). Дерево доказательства. Секвенции. Формат команд. Основные команды.
Генерация формул корректности в виде теорий на языке PVS на примере программ целочисленных стандартных функций.
2.3. Автоматное программирование
Основы. Классы программ. Принципиальное свойство разграничения программ-функций и программ-процессов. Общее определение автоматной программы и определение на примере. Системы автоматного программирования. Графический язык Дракон.
Класс реактивных систем. Системы автоматического управления. Системы реального времени.
Язык требований. Условия. Действия. Семантика исполнения.
Базисы автоматного программирования.
Объектно-ориентированное расширение. Языковые конструкции. Инвариант класса. Условия корректности.
Язык автоматных программ. Управляющие состояния. Сегменты кода. Состояние программы. Сообщения. Языковые средства. Операторы приема и посылки сообщений. Средства работы со временем.
Декомпозиция простых процессов.
Золотые правила программирования.
Примеры. Функционирование лампочки. Другой вид языка требований. Рыбная ловля. Электронные часы с будильником. Гадание на кофейных зернах. Управление лифтом.
Коммуникационные протоколы. Протокол чередования битов. Протокол скользящего окна. Протокол рукопожатия.
Трансформация требований: эквивалентные замены, специализация,
редукция суперпозиции. Пример: протокол AAL-2.
Раздел 3. Верификация программных систем методом проверки моделей
3.1. Метод проверки моделей: спецификация и моделирование систем
Введение. Обоснование применения метода проверки моделей. Надежность программ и систем. Логический язык спецификаций. Понятие корректности программных систем.
Моделирование систем. Структура Крипке. Логическое представление программных систем. Примеры параллельных и взаимодействующих систем.
Спецификация программных систем с помощью временных логик CTL и LTL.
Спецификация типичных свойств моделей систем. Достижимость, живость, безопасность, справедливость, выигрыш.
3.2. Проверка моделей на практике: инструменты и типичные задачи
Инструменты проверки моделей SPIN и SMV. Примеры.
Примеры типичных задач для метода проверки моделей. Анализ бизнес-процессов. Планирование. Головоломки. Криптографические протоколы.
3.3. Алгоритмы проверки моделей: классические и оптимизированные
Алгоритмы проверки на модели свойств систем, выраженных формулами временных логик CTL и LTL.
Символьные представления данных для алгоритмов проверки моделей. Булевские модели. Целочисленные модели.
Символьный алгоритм проверки на модели свойств систем, выраженных формулами временной логики CTL. Справедливость. Контрпримеры и свидетельства.
Символьный алгоритм проверки на модели свойств систем, выраженных формулами временной логики LTL.
Использование особенностей проверяемых моделей: редукция, абстракция, композиция, симметрия.
Раздел 4. Методы спецификации и анализа терминологических систем
4.1. Моделирование терминологических систем на основе логических методов
Введение. Обоснование применения логики для формализации терминологий. Основания дескрипционных логик. Синтаксис и семантика языков EL и ALC. Трансляция в логику первого порядка. Связь с логическим программированием и модальными логиками.
Использование дескрипционных логик для формализации терминологических систем. Задача классификации терминов. Проблема невырожденности термина. Сложность логического вывода. Канонические модели, кодирование бинарных счетчиков. Основы работы в системе Protégé.
4.2. Методы автоматического доказательства в дескрипционных логиках
Метод прямого вывода для логики EL. Табличный вывод для ALC. Стандартные техники оптимизации табличного вывода. Нормализация и развертывание аксиом. Замена определений и абсорбция. Оптимизации в задаче классификации терминов.
Комбинированный вывод для ALC. Объяснение свойств терминологических систем на основе доказательств. Проблема объяснения противоречий. Использование машин вывода ELK и Fact++ в системе Protégé.
4.3. Анализ терминологических систем на основе логического вывода
Явные терминологические определения. Переименования и интерполяция Крейга. Построение явных определений из доказательств.
Вычисление компонент в терминологических системах. Сильнейшие следствия, униформная интерполяция и стирание. Следствия за пределами языка. Свойство неотделимости. Семантические/синтаксические компоненты. Декомпозиция терминологических систем. Связь с явными определениями. Расширения HyperMod и OWLDiff для Protégé.
Терминологические запросы к базам данных. Первопорядковое переписывание запросов. Переписывание через интерполяцию. Расширение Ontop для Protégé.
Список основной и дополнительной литературы по разделу 1
1. Л., А. Математическая логика. : Наука, 1987. – 336 с.
2. Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T), Journal of the ACM (JACM), Volume 53 Issue 6, November 2006, pp. 937–977.
3. Википедия, статьи:
https://en. wikipedia. org/wiki/Boolean_satisfiability_problem
https://en. wikipedia. org/wiki/DPLL_algorithm
https://en. wikipedia. org/wiki/Conflict-Driven_Clause_Learning
https://en. wikipedia. org/wiki/Satisfiability_modulo_theories
4. David R. Cok. The SMT-LIBv2 Language and Tools: A Tutorial
http://www. /resource/smt/SMTLIBTutorial. pdf
5. Bruno Dutertre. Yices Manual. http://yices. csl. /papers/manual. pdf
6. Z3 Documentation. https:///Z3Prover/z3/wiki/Documentation
Список основной и дополнительной литературы по разделу 2
а) основная литература:
1. И. Предикатное программирование. Учебное пособие. — НГУ, Новосибирск, 2009. — 109с.
2. И. Формальные методы в описании языков и систем программирования. Электронный учебник. — НГУ, Новосибирск, 2011. — 118с.
3. И. Семантика языка предикатного программирования // ЗОНТ-15. — Новосибирск, 2015. — 13с. http://persons. iis. /files/persons/pages/semZont1.pdf
4. С., Ю., И. Язык предикатного программирования P. Версия 0.12 — Новосибирск, 2014. — 28с. http://persons. iis. /files/persons/pages/plang12.pdf
5. И. Язык и технология автоматного программирования // «Программная инженерия», №4, 2014. – C. 3-15. http://persons. iis. /files/persons/pages/automatProg. pdf
6. И. Разработка автоматных программ на базе определения требований // Системная информатика, №4, 2014. — ИСИ СО РАН, Новосибирск. — C. 1-29. http://persons. iis. /files/persons/pages/req_tech. pdf
7. С. Система дедуктивной верификации предикатных программ // Тр. 2-й межд. конф. «Инструменты и методы анализа программ». – Кострома, Костромской государственный технологический университет. — 14-15 ноября 2014г. — С. 205-214. http://tmpaconf. org/images/pdf/2014/michael%20chushkin. pdf
б) дополнительная литература:
1. И. Оптимизация автоматных программ методом трансформации требований // Тр. 2-й межд. конф. «Инструменты и методы анализа программ». – Кострома, Костромской государственный технологический университет. — 14-15 ноября 2014г. — С. 175-183. http://persons. iis. /files/persons/pages/req_k. pdf
2. И. Верификация и синтез эффективных программ стандартных функций в технологии предикатного программирования // Программная инженерия, 2011, № 2. ¾ С. 14-21.
3. Методы предикатного программирования. Вып.1— Сборник работ ИСИ СО РАН под ред. И. — Новосибирск, 2003.
4. Методы предикатного программирования. Вып.2— Сборник работ ИСИ СО РАН под ред. И. — Новосибирск, 2006.
в) программное обеспечение и Интернет-ресурсы:
1. PVS Language Reference. Version 2.4. — SRI International. 2001. — http://pvs. csl. /doc/pvs-language-reference. pdf
Список основной и дополнительной литературы по разделу 3.
а) основная литература:
1. Г. Model Checking. Верификация параллельных и распределенных программных систем. ─ СПб.: «БХВ-Петербург», 2010. ─ 560 с.
2. Clarke E. M., Grumberg O., Peled D. Model Checking. ─ London: MIT Press, 1999. ─ 314 p. (Pусский перевод: Э. М.Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ: Model Checking. М., 2002)
3. Gerard J. Holzmann. Spin Model Checker, The: Primer and Reference Manual ─ Addison Wesley, 2003 ─ 608 c.
б) дополнительная литература:
1. Bultan T., Gerber R., and Pugh W. Model Checking Concurrent Systems With Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results // ACM Trans. Progr. Lang, and Systems ─ 1999. ─ Vol. 21, N 4 ─ P. 747-789.
2. B. Boigelot and P. Wolper. Symbolic Verification with Periodic Sets // Lect. Notes Comput. Sci. ─ Berlin etc., 1994. ─ Vol. 818. ─ P. 55-67.
3. О. Верификация распределенных систем с использованием аффинного представления данных, логик знаний и действий. Диссертация на соискание ученой степени кандидата физико-математических наук ─ Новосибирск, 2004. ─ 172 с.
в) программное обеспечение и Интернет-ресурсы:
1. Иинструмент верификации моделей Spin – url:
http:///spin/whatispin. html
2. Инструмент верификации моделей SMV – url:
http://www. cs. cmu. edu/~modelcheck/smv. html.
Список основной и дополнительной литературы по разделу 4.
a) основная литература:
1. Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementation, and Applications. // Cambridge University Press, 2nd edition, 2010 — 624 p.
2. Искусственный интеллект: современный подход. — М.: ИД «Вильямс», 2006. — 1408 с.
3. В. Формализмы и средства создания и поддержки онтологий. — С., В., И., А., С., Г., А., А., А., В. Модели и методы построения информационных систем, основанных на формальных, логических и лингвистических подходах // Моногр. / Институт систем информатики им. А. П. Ершова СО РАН. — Новосибирск: Изд. СО РАН, 2009 — 240 с.
b) дополнительная литература:
1. Boris Konev, Carsten Lutz, Dirk Walther, and Frank Wolter. Formal Properties of Modularisation. In: Stuckenschmidt, H., Parent, C., Spaccapietra, S. (Eds.), Modular Ontologies. — vol. 5445 of Lecture Notes in Computer Science, Springer, 2008 — pp. 25– 66. http://www. csc. liv. ac. uk/~frank/publ/modulebook. pdf
2. Roman Kontchakov and Mikhail Zakharyaschev. An Introduction to Description Logics and Query Rewriting. In M. Koubarakis, G. Stamou and G. Stoilos, editors, Reasoning Web Summer School (Athens, 8-13 September), — vol. 8714 of LNCS, Springer, 2014. — pp. 195-244.
http://www. dcs. bbk. ac. uk/~roman/papers/RW12014.pdf
3. Boris Konev, Carsten Lutz, Denis Ponomaryov, and Frank Wolter, Decomposing Description Logic Ontologies. — In: Lin, F., Sattler, U., Truszczynski, M. (Eds.), KR 2010. AAAI Press. http://persons. iis. /files/persons/pages/ontdecomp. pdf
4. Denis Ponomaryov and Dmitry Vlasov. Concept Definability and Interpolation in Enriched Models of EL-Tboxes. In: Eiter, T., Glimm, B., Kazakov, Y., Krötzsch, M. (Eds.), Description Logics. — vol. 1014 of CEUR Workshop Proceedings. CEUR - WS. org, 2013. — pp. 898–916. http://persons. iis. /files/persons/pages/conceptinterpolation. pdf
5. Bernardo Cuenca Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler. Modular Reuse of Ontologies: Theory and practice. — J. Artif. Int. Res. 31 (1), 2008. — pp. 273–318. https://www. cs. ox. ac. uk/files/4559/live-2375-3703-jair. pdf
6. Matthew Horridge. Justification Based Explanation in Ontologies. — PhD Thesis. University of Manchester, 2011. — 278 p. https://www. escholar. manchester. ac. uk/api/datastream? publicationPid=uk-ac-man-scw:131699&datastreamId=FULL-TEXT. PDF
7. Dmitry Tsarkov, Ian Horrocks, and Peter F. Patel-Schneider. Optimizing Terminological Reasoning for Expressive Description Logics. — J. of Automated Reasoning, 39(3), 2007. — pp. 277-316. http://www. cs. man. ac. uk/~tsarkov/papers/TsHP07a. pdf
8. Yevgeny Kazakov, Markus Krötzsch, and František Simančík. The Incredible ELK. — Journal of Automated Reasoning — vol. 53, Issue 1, 2014 — pp. 1-61. http://elk. semanticweb. org/publications/incredible-elk-jar-2013.pdf
в) программное обеспечение и Интернет-ресурсы
1. Шаблоны в моделировании терминологических систем http://ontologydesignpatterns. org/wiki/Main_Page
2. Документация системы Protégé http://protegewiki. stanford. edu/wiki/Protege4UserDocs
3. Документация расширения Ontop для Protégé http://ontop. inf. unibz. it/documentation/
4. Документация расширения OWLDiff для Protégé http://krizik. felk. cvut. cz/km/owldiff/documentation. html
Основные порталы (построено редакторами)