Формальные методы

Пример формальной спецификации с использованием Z-нотации

В информатике и инженерии программного обеспечения формальными методами (англ. formal methods) называется группа техник, основанных на математическом аппарате для спецификации, разработки и верификации программного и аппаратного обеспечения[1]. Использование формальных методов для проектирования программного и аппаратного обеспечения обусловлено ожиданиями того, что, как и в других инженерных областях, использование математического анализа может существенно поднять надёжность систем[2]. При этом формальные методы довольно сложны, требуют специальной подготовки, временных и ресурсных вложений, и при этом нередко основываются на не всегда достижимых в реальных условиях предположениях. Это приводит к тому, что формальные методы чаще всего находят применение в проектировании высокоточных систем, где важность безопасности оправдывает любые средства.

Формальные методы занимаются приложением довольно широкого класса фундаментальных техник теоретической информатики: разные исчисления логики, формальных языков, теории автоматов, формальной семантики, систем типов и алгебраических типов данных[3].

Разновидности формальных методов

[править | править код]

Можно выделить три уровня применения формальных методов:

Нулевой уровень
Разрабатывается формальная спецификация, затем программный код пишется, глядя на неё. В этом случае пропасть между формальной и неформальной частью остаётся бездоказательной, но решение может быть эффективным с точки зрения его стоимости.
Первый уровень
Программный код выводится из формальной спецификации автоматически, используются механизмы верификации, доказываются наиболее критичные свойства системы. Этот путь зачастую выбирается для высокоточных систем.
Второй уровень
Автоматические доказатели теорем используются для выведения полностью формализованных доказательств, проверяемых автоматически. Подход требует объёмных вложений и исследований, но оправдывает себя в самых критичных частях сложных систем, где ошибки непозволительны (например, в проектировании интегральных схем).

Подходы к формальным методам также можно классифицировать аналогично формальной семантике языков программирования:

Денотационная семантика (англ. denotational semantics)
Значение системы выражается через частично упорядоченные множества, а методы полагаются на хорошо разработанную теорию вокруг них. Ограничение метода — в том, что не каждая система может быть интуитивно или естественно рассмотрена как функция.
Операционная семантика (англ. operational semantics)
Значение системы обозначается последовательностью действий в рамках более простой вычислительной модели (например, лямбда-исчисления или сетей Петри). Методы славятся своей простотой, если не акцентировать внимание на том, что они полагаются на семантику «более простой» системы, которую тоже надо через что-то определять.
Аксиоматическая семантика (англ. axiomatic semantics)
Смысл системы определяется в терминах предусловий и постусловий, что позволяет связать теорию с классической логикой, но не даёт представления о том, что конкретно происходит внутри системы (как достигаются постусловия на основе предусловий).

Кроме того, нередко резко положительных результатов можно достичь, пожертвовав глобальной применимостью и сверхформализацией — такие случаи называют «облегчёнными» (lightweight) формальными методами. Их можно разделить на два типа: с усиленной и с ослабленной автоматизацией. Пример усиленной автоматизации — анализатор спецификаций Alloy Analyzer, который для того, чтобы свести задачу поиска модели к решаемой, сужая область поиска (в результате Аллой работает полностью автоматизированно, в отличие от интерактивных доказателей, но имеет шанс не найти некоторые проблемы). Пример ослабленной — сходимость грамматик, в которой неразрешимость задачи эквивалентности двух формальных языков обходится тем, что преобразования совершает сам человек, а выводы делаются уже по свойствам использованных им операторов.

Использование формальных методов

[править | править код]

Формальные методы применяются на разных этапах разработки программного обеспечения:

Спецификация
С помощью формальных методов можно описать будущую систему с любым уровнем детализации. Такое формальное описание может напрямую или опосредовано с пользой использоваться на более поздних этапах. При этом работа по доказательству ряда требуемых функциональных свойств может начинаться сразу и идти параллельно с написанием или генерацией кода. Существует целый ряд языков и исчислений для формальных спецификаций, но ни один не может претендовать на звание универсального, как Форма Бэкуса — Наура для спецификации синтаксиса.
Разработка
Если формальная спецификация использует операциональную семантику, наблюдаемое поведение конкретной системы можно сравнивать с ожидаемым, потому что такая семантика может быть выполнимой, а может даже использоваться для автоматического генерирования кода. Если используется аксиоматическая семантика, то предусловия и постусловия могут напрямую отобразиться в утверждения в выполнимом коде.
Верификация
Когда формальная спецификация подготовлена, её можно использовать для доказательства требуемых свойств. Верификация бывает дедуктивной и модельной: дедуктивная использует автоматическое доказательство теорем или специфические алгебры, а модельная основывает свои выводы не на самой системе, а на построенной по ней модели[4]. При этом модель совершенно не обязательно строить вручную, если применимы оказываются техники вроде программного сечения[англ.].

Критика формальных методов

[править | править код]

Доказательства вручную требуют серьёзных вложений ресурсов и не дают никакой выгоды, кроме подтверждения правильности. В результате формальные методы используются или в тех областях, где доказательства можно получить автоматически программным путём, или в тех, где цена ошибки слишком высока (например, при создании космических аппаратов или магнитно-резонансных томографов).

Абстракции, нотации и языки формальных методов

[править | править код]

Примечания

[править | править код]
  • Jean François Monin, Michael Gerard Hinchey, Understanding formal methods, Springer, 2003, ISBN 1852332476
  1. ↑ R. W. Butler. What is Formal Methods? (6 августа 2001). Дата обращения: 16 ноября 2006. Архивировано 25 августа 2012 года.
  2. ↑ C. Michael Holloway. Why Engineers Should Consider Formal Methods (неопр.). — 16th Digital Avionics Systems Conference (27–30 October 1997). Архивировано 23 июля 2018 года.
  3. ↑ Monin, pp.3-4
  4. ↑ Верификация программ с помощью моделей Архивная копия от 21 февраля 2010 на Wayback Machine, «Открытые системы» , № 12, 2003.

Литература

[править | править код]
  • Lathouwers, Sophie; Zaytsev, Vadim (2022). "Modelling Program Verification Tools for Software Engineers". Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems. MODELS '22. Montreal, Quebec, Canada: Association for Computing Machinery. pp. 98—108. doi:10.1145/3550355.3552426. ISBN 9781450394666.

Ссылки

[править | править код]
Источник — https://ru.wikipedia.org/w/index.php?title=Формальные_методы&oldid=134982882