В информатике и инженерии программного обеспечения формальными методами называется группа техник, основанных на математическом аппарате для спецификации, разработки и верификации программного и аппаратного обеспечения[1]. Использование формальных методов для проектирования программного и аппаратного обеспечения обусловлено ожиданиями того, что, как и в других инженерных областях, использование математического анализа может существенно поднять надёжность систем[2]. При этом формальные методы довольно сложны, требуют специальной подготовки, временных и ресурсных вложений, и при этом нередко основываются на не всегда достижимых в реальных условиях предположениях. Это приводит к тому, что формальные методы чаще всего находят применение в проектировании высокоточных систем, где важность безопасности оправдывает любые средства.
Формальные методы занимаются приложением довольно широкого класса фундаментальных техник теоретической информатики: разные исчисления логики, формальных языков, теории автоматов, формальной семантики, систем типизации и алгебраических типов данных[3].
Разновидности формальных методов
Можно выделить три уровня применения формальных методов:
- Нулевой уровень
- Разрабатывается формальная спецификация, затем программный код пишется, глядя на неё. В этом случае пропасть между формальной и неформальной частью остаётся бездоказательной, но решение может быть эффективным с точки зрения его стоимости.
- Первый уровень
- Программный код выводится из формальной спецификации автоматически, используются механизмы верификации, доказываются наиболее критичные свойства системы. Этот путь зачастую выбирается для высокоточных систем.
- Второй уровень
- Автоматические доказатели теорем используются для выведения полностью формализованных доказательств, проверяемых автоматически. Подход требует объёмных вложений и исследований, но оправдывает себя в самых критичных частях сложных систем, где ошибки непозволительны (например, в проектировании интегральных схем).
Подходы к формальным методам также можно классифицировать аналогично формальной семантике языков программирования:
- Денотационная семантика
- Значение системы выражается через частично упорядоченные множества, а методы полагаются на хорошо разработанную теорию вокруг них. Ограничение метода — в том, что не каждая система может быть интуитивно или естественно рассмотрена как функция.
- Операциональная семантика
- Значение системы обозначается последовательностью действий в рамках более простой вычислительной модели (например, лямбда-исчисления или сетей Петри). Методы славятся своей простотой, если не акцентировать внимание на том, что они полагаются на семантику «более простой» системы, которую тоже надо через что-то определять.
- Аксиоматическая семантика
- Смысл системы определяется в терминах предусловий и постусловий, что позволяет связать теорию с классической логикой, но не даёт представления о том, что конкретно происходит внутри системы (как достигаются постусловия на основе предусловий).
Кроме того, нередко резко положительных результатов можно достичь, пожертвовав глобальной применимостью и сверхформализацией — такие случаи называют «облегчёнными» (lightweight) формальными методами. Их можно разделить на два типа: с усиленной и с ослабленной автоматизацией. Пример усиленной автоматизации — анализатор спецификаций Alloy Analyzer, который для того, чтобы свести задачу поиска модели к решаемой, сужая область поиска (в результате Аллой работает полностью автоматизированно, в отличие от интерактивных доказателей, но имеет шанс не найти некоторые проблемы). Пример ослабленной — сходимость грамматик, в которой неразрешимость задачи эквивалентности двух формальных языков обходится тем, что преобразования совершает сам человек, а выводы делаются уже по свойствам использованных им операторов.
Использование формальных методов
Формальные методы применяются на разных этапах цикла разработки программного обеспечения:
- Спецификация
- С помощью формальных методов можно описать будущую систему с любым уровнем детализации. Такое формальное описание может напрямую или опосредовано с пользой использоваться на более поздних этапах. При этом работа по доказательству ряда требуемых функциональных свойств может начинаться сразу и идти параллельно с написанием или генерацией кода. Существует целый ряд языков и исчислений для формальных спецификаций, но ни один не может претендовать на звание универсального, как Форма Бэкуса — Наура для спецификации синтаксиса.
- Разработка
- Если формальная спецификация использует операциональную семантику, наблюдаемое поведение конкретной системы можно сравнивать с ожидаемым, потому что такая семантика может быть выполнимой, а может даже использоваться для автоматического генерирования кода. Если используется аксиоматическая семантика, то предусловия и постусловия могут напрямую отобразиться в утверждения в выполнимом коде.
- Верификация
- Когда формальная спецификация подготовлена, её можно использовать для доказательства требуемых свойств. Верификация бывает дедуктивной и модельной: дедуктивная использует автоматическое доказательство теорем или специфические алгебры, а модельная основывает свои выводы не на самой системе, а на построенной по ней модели[4]. При этом модель совершенно не обязательно строить вручную, если применимы оказываются техники вроде программного сечения (англ.).
Критика формальных методов
Легко догадаться, какие претензии предъявляются к формальным методам: доказательства вручную требуют серьёзных вложений времени (а значит, и денег) и не дают никакой выгоды, кроме подтверждения правильности. В результате формальные методы используются или в тех областях, где доказательства можно получить автоматически программным путём, или в тех, где цена ошибки слишком высока. Например, при создании космических аппаратов или магнитно-резонансных томографов необнаруженные ошибки приводят к гибели людей, а при проектировании интерфейсов пользователя или браузеров — в худшем случае к порче настроения, поэтому в первых двух случаях формальные методы будут применяться, а в последних — нет.
Абстракции, нотации и языки формальных методов
Примечания
- Jean François Monin, Michael Gerard Hinchey, Understanding formal methods, Springer, 2003, ISBN 1852332476
- What is Formal Methods? (6 августа 2001). Проверено 16 ноября 2006.
- Why Engineers Should Consider Formal Methods» (16th Digital Avionics Systems Conference (27–30 October 1997)). Проверено 2006-11-16.
- ↑ Monin, pp.3-4
- Верификация программ с помощью моделей, «Открытые системы» , № 12, 2003.
Ссылки