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