2024/2025
Формальные методы программной инженерии
Статус:
Маго-лего
Кто читает:
Департамент программной инженерии
Когда читается:
2-4 модуль
Охват аудитории:
для своего кампуса
Язык:
русский
Кредиты:
9
Контактные часы:
116
Программа дисциплины
Аннотация
В информатике и разработке программного обеспечения формальные методы представляют собой особый вид математически обоснованных методов для спецификации, разработки и верификации программных и аппаратных систем. Использование формальных методов для проектирования программного и аппаратного обеспечения мотивировано тем фактом, что, как и в других инженерных дисциплинах, выполнение соответствующего математического анализа может способствовать повышению надежности проекта. Формальные методы лучше всего описать как применение довольно широкого спектра теоретических основ информатики, в частности логических исчислений, формальных языков, теории автоматов и семантики программ, а также систем типов и алгебраических типов данных к задачам спецификации и верификации программного и аппаратного обеспечения. Формальные методы могут: (а) быть основой для описания сложных систем; (б) быть основой для рассуждений о системах; (в) обеспечивать поддержку разработки программ. В отличие от других подходов к проектированию систем, формальные методы используют математическое доказательство в качестве дополнения к системному тестированию для обеспечения правильного поведения. Поскольку системы усложняются, а безопасность становится все более важным вопросом, формальный подход к проектированию систем предлагает другой уровень страхования. Формальные методы отличаются от других методов проектирования использованием формальных схем проверки, правильность основных принципов системы должна быть доказана до того, как они будут приняты. Традиционный дизайн системы использует обширное тестирование для проверки поведения, но тестирование способно дать лишь конечные выводы. Э. Дейкстра и другие продемонстрировали, что тесты могут помочь обнаружить сбои и баги, но не могут гарантировать их отсутствие. Напротив, как только теорема доказана, она остается истинной. Очень важно отметить, что формальная проверка не устраняет необходимости в тестировании. Формальная проверка не может исправить неверные предположения в проекте, но она может помочь выявить ошибки в рассуждениях, которые в противном случае остались бы непроверенными. В нескольких случаях инженеры сообщали об обнаружении недостатков в системах после того, как они официально рассмотрели свои проекты.