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

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

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

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

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

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

Нулевой уровень

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

Первый уровень

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

Второй уровень

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

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

Денотационная семантика

Значение системы выражается через частично упорядоченные множества, а методы полагаются на хорошо разработанную теорию вокруг них. Ограничение метода — в том, что не каждая система может быть интуитивно или естественно рассмотрена как функция.

Операциональная семантика

Значение системы обозначается последовательностью действий в рамках более простой вычислительной модели (например, лямбда-исчисления или сетей Петри). Методы славятся своей простотой, если не акцентировать внимание на том, что они полагаются на семантику «более простой» системы, которую тоже надо через что-то определять.

Аксиоматическая семантика

Смысл системы определяется в терминах предусловий и постусловий, что позволяет связать теорию с классической логикой, но не даёт представления о том, что конкретно происходит внутри системы (как достигаются постусловия на основе предусловий).

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

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

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

Спецификация

С помощью формальных методов можно описать будущую систему с любым уровнем детализации. Такое формальное описание может напрямую или опосредовано с пользой использоваться на более поздних этапах. При этом работа по доказательству ряда требуемых функциональных свойств может начинаться сразу и идти параллельно с написанием или генерацией кода. Существует целый ряд языков и исчислений для формальных спецификаций, но ни один не может претендовать на звание универсального, как Форма Бэкуса — Наура для спецификации синтаксиса.

Разработка

Если формальная спецификация использует операциональную семантику, наблюдаемое поведение конкретной системы можно сравнивать с ожидаемым, потому что такая семантика может быть выполнимой, а может даже использоваться для автоматического генерирования кода. Если используется аксиоматическая семантика, то предусловия и постусловия могут напрямую отобразиться в утверждения в выполнимом коде.

Верификация

Когда формальная спецификация подготовлена, её можно использовать для доказательства требуемых свойств. Верификация бывает дедуктивной и модельной: дедуктивная использует автоматическое доказательство теорем или специфические алгебры, а модельная основывает свои выводы не на самой системе, а на построенной по ней модели^[4]. При этом модель совершенно не обязательно строить вручную, если применимы оказываются техники вроде программного сечения (англ.).

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

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

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

• Абстрактная интерпретация (англ.)
• Абстрактный автомат (ASM)
  • Конечный автомат (FSM)
  • Машина Тьюринга
  • Модель Крипке
• Автомат Бюхи (англ.)
• Alloy Analyzer (англ.)
• Анализ программного кода и построенных по нему графов:
  • Анализ потока данных (англ.) (DFA)
  • Анализ потока управления (CFA)
  • Динамический анализ кода
  • Статический анализ кода
• B-метод (англ.)
• Венский метод разработки (англ.) (VDM, VDM-SL, VDM+)
• Единый язык алгебраических спецификаций (англ.) (CASL) и программа Hets
• Исчисления процессов:
  • Алгебра общающихся систем (англ.) (ACP)
  • Взаимодействующие последовательные процессы (англ.) Хоара (CSP)
  • Исчисление общающихся систем
  • пи-исчисление
  • Язык спецификации временного упорядочивания (англ.) (LOTOS)
• Lustre (англ.)
• Лямбда-исчисление, включая типизированное
• Модель акторов
• Переписывание (TRS)
• Промела (англ.) и верификатор моделей SPIN (англ.)
• Ребека (англ.)
• Сети Петри
• Создание и анализ распределённых процессов (англ.) (CADP)
• Темпоральная логика (особенно TLA+ и PlusCal)
• Универсальный язык систем (англ.) (USL)
• Эстерел (англ.)
• Язык спецификации ANSI/ISO C (англ.) (ACSL) и верификатор Frama-C
• Язык спецификации и описания (англ.) (SDL)
• Z-нотация

Примечания

• Jean François Monin, Michael Gerard Hinchey, Understanding formal methods, Springer, 2003, ISBN 1852332476

1. ↑ R. W. Butler What is Formal Methods? (6 августа 2001). Архивировано из первоисточника 25 августа 2012. Проверено 16 ноября 2006.
2. ↑ C. Michael Holloway. «Why Engineers Should Consider Formal Methods» (16th Digital Avionics Systems Conference (27–30 October 1997)). Проверено 2006-11-16.
3. ↑ Monin, pp.3-4
4. ↑ Верификация программ с помощью моделей, «Открытые системы» , № 12, 2003.

Ссылки

• Викия по формальным методам
• Formal Methods Europe (FME)
• FM — Международный симпозиум по формальным методам, престижная конференция
• ICFEM — Международная конференция по формальным инженерным методам, конференция IEEE ненамного ниже уровнем
• IFM — Международная конференция по интегрированным формальным методам, конференция одного уровня с ICFEM