Магистратура 2024/2025

Формальные методы программной инженерии

Статус: Курс обязательный (Системная и программная инженерия)

Направление: 09.04.04. Программная инженерия

Кто читает: Департамент программной инженерии

Где читается: Факультет компьютерных наук

Когда читается: 1-й курс, 2-4 модуль

Формат изучения: без онлайн-курса

Охват аудитории: для своего кампуса

Преподаватели: Ломазова Ирина Александровна, Нестеров Роман Александрович

Прогр. обучения: Системная и программная инженерия

Язык: русский

Кредиты: 9

Программа дисциплины

Аннотация

В информатике и разработке программного обеспечения формальные методы представляют собой особый вид математически обоснованных методов для спецификации, разработки и верификации программных и аппаратных систем. Использование формальных методов для проектирования программного и аппаратного обеспечения мотивировано тем фактом, что, как и в других инженерных дисциплинах, выполнение соответствующего математического анализа может способствовать повышению надежности проекта. Формальные методы лучше всего описать как применение довольно широкого спектра теоретических основ информатики, в частности логических исчислений, формальных языков, теории автоматов и семантики программ, а также систем типов и алгебраических типов данных к задачам спецификации и верификации программного и аппаратного обеспечения. Формальные методы могут: (а) быть основой для описания сложных систем; (б) быть основой для рассуждений о системах; (в) обеспечивать поддержку разработки программ. В отличие от других подходов к проектированию систем, формальные методы используют математическое доказательство в качестве дополнения к системному тестированию для обеспечения правильного поведения. Поскольку системы усложняются, а безопасность становится все более важным вопросом, формальный подход к проектированию систем предлагает другой уровень страхования. Формальные методы отличаются от других методов проектирования использованием формальных схем проверки, правильность основных принципов системы должна быть доказана до того, как они будут приняты. Традиционный дизайн системы использует обширное тестирование для проверки поведения, но тестирование способно дать лишь конечные выводы. Э. Дейкстра и другие продемонстрировали, что тесты могут помочь обнаружить сбои и баги, но не могут гарантировать их отсутствие. Напротив, как только теорема доказана, она остается истинной. Очень важно отметить, что формальная проверка не устраняет необходимости в тестировании. Формальная проверка не может исправить неверные предположения в проекте, но она может помочь выявить ошибки в рассуждениях, которые в противном случае остались бы непроверенными. В нескольких случаях инженеры сообщали об обнаружении недостатков в системах после того, как они официально рассмотрели свои проекты.

Цель освоения дисциплины

• изучение методов формальной спецификации и верификации поведения последовательных и параллельных систем с помощью различных подходов
• изучение методов model checking для спецификации и верификации поведения распределенных информационных систем

Планируемые результаты обучения

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

Содержание учебной дисциплины

• Формальные методы как основа надежности программного обеспечения
• Дедуктивная верификация программ. Логика Хоара
• Конечные автоматы
• Сети Петри
• Процессные алгебры
• Бисимуляция
• Concurrency Workbench: практика моделирования с помощью алгебры CCS
• Model Checking: введение
• Model Checking: свойства линейного времени, регулярные свойства
• Model Checking: темпоральная логика линейного времени LTL
• Model checking: практика верификации формул логики LTL
• Model checking: логика ветвящегося времени CTL

Элементы контроля

• O_accum1
  Выполнение заданий на семинарах
• O_exam1
• O_accum2
• O_htask2
• O_exam2

Промежуточная аттестация

• 2024/2025 2nd module
  0.5 * O_accum1 + 0.5 * O_exam1
• 2024/2025 4th module
  0.12 * 2024/2025 2nd module + 0.3 * O_accum2 + 0.4 * O_exam2 + 0.18 * O_htask2

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

Рекомендуемая основная литература

• Baeten, J. C. M., Reniers, M. A., & Basten, T. G. H. (2010). Process Algebra: Equational Theories of Communicating Processes. Cambridge: Cambridge University Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=317653
• Baier, C., & Katoen, J.-P. (2008). Principles of Model Checking. Cambridge, Mass: The MIT Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=226091
• Fisher, M. (2011). An Introduction to Practical Formal Methods Using Temporal Logic. Chichester, West Sussex, U.K.: Wiley. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=509889
• Wolfgang Reisig. (2013). Understanding Petri Nets : Modeling Techniques, Analysis Methods, Case Studies (Vol. 2013). Springer.

Рекомендуемая дополнительная литература

• Wan Fokkink, Jan Friso Groote, & Michel Reniers. (2003). Modelling Distributed Systems. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsbas&AN=edsbas.E2E909CB
• Wil van der Aalst, & Kees van Hee. (2004). Workflow Management: Models, Methods, and Systems. The MIT Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsrep&AN=edsrep.b.mtp.titles.0262720469

Авторы

• Нестеров Роман Александрович
• Петрухина Анастасия Сергеевна