Русская Википедия:Формальные методы
В информатике и инженерии программного обеспечения формальными методами (Шаблон:Lang-en) называется группа техник, основанных на математическом аппарате для спецификации, разработки и верификации программного и аппаратного обеспечения[1]. Использование формальных методов для проектирования программного и аппаратного обеспечения обусловлено ожиданиями того, что, как и в других инженерных областях, использование математического анализа может существенно поднять надёжность систем[2]. При этом формальные методы довольно сложны, требуют специальной подготовки, временных и ресурсных вложений, и при этом нередко основываются на не всегда достижимых в реальных условиях предположениях. Это приводит к тому, что формальные методы чаще всего находят применение в проектировании высокоточных систем, где важность безопасности оправдывает любые средства.
Формальные методы занимаются приложением довольно широкого класса фундаментальных техник теоретической информатики: разные исчисления логики, формальных языков, теории автоматов, формальной семантики, систем типов и алгебраических типов данных[3].
Разновидности формальных методов
Можно выделить три уровня применения формальных методов:
- Нулевой уровень
- Разрабатывается формальная спецификация, затем программный код пишется, глядя на неё. В этом случае пропасть между формальной и неформальной частью остаётся бездоказательной, но решение может быть эффективным с точки зрения его стоимости.
- Первый уровень
- Программный код выводится из формальной спецификации автоматически, используются механизмы верификации, доказываются наиболее критичные свойства системы. Этот путь зачастую выбирается для высокоточных систем.
- Второй уровень
- Автоматические доказатели теорем используются для выведения полностью формализованных доказательств, проверяемых автоматически. Подход требует объёмных вложений и исследований, но оправдывает себя в самых критичных частях сложных систем, где ошибки непозволительны (например, в проектировании интегральных схем).
Подходы к формальным методам также можно классифицировать аналогично формальной семантике языков программирования:
- Шаблон:Нп2
- Значение системы выражается через частично упорядоченные множества, а методы полагаются на хорошо разработанную теорию вокруг них. Ограничение метода — в том, что не каждая система может быть интуитивно или естественно рассмотрена как функция.
- Шаблон:Нп2
- Значение системы обозначается последовательностью действий в рамках более простой вычислительной модели (например, лямбда-исчисления или сетей Петри). Методы славятся своей простотой, если не акцентировать внимание на том, что они полагаются на семантику «более простой» системы, которую тоже надо через что-то определять.
- Шаблон:Нп2
- Смысл системы определяется в терминах предусловий и постусловий, что позволяет связать теорию с классической логикой, но не даёт представления о том, что конкретно происходит внутри системы (как достигаются постусловия на основе предусловий).
Кроме того, нередко резко положительных результатов можно достичь, пожертвовав глобальной применимостью и сверхформализацией — такие случаи называют «облегчёнными» (lightweight) формальными методами. Их можно разделить на два типа: с усиленной и с ослабленной автоматизацией. Пример усиленной автоматизации — анализатор спецификаций Alloy Analyzer, который для того, чтобы свести задачу поиска модели к решаемой, сужая область поиска (в результате Аллой работает полностью автоматизированно, в отличие от интерактивных доказателей, но имеет шанс не найти некоторые проблемы). Пример ослабленной — сходимость грамматик, в которой неразрешимость задачи эквивалентности двух формальных языков обходится тем, что преобразования совершает сам человек, а выводы делаются уже по свойствам использованных им операторов.
Использование формальных методов
Формальные методы применяются на разных этапах разработки программного обеспечения:
- Спецификация
- С помощью формальных методов можно описать будущую систему с любым уровнем детализации. Такое формальное описание может напрямую или опосредовано с пользой использоваться на более поздних этапах. При этом работа по доказательству ряда требуемых функциональных свойств может начинаться сразу и идти параллельно с написанием или генерацией кода. Существует целый ряд языков и исчислений для формальных спецификаций, но ни один не может претендовать на звание универсального, как Форма Бэкуса — Наура для спецификации синтаксиса.
- Разработка
- Если формальная спецификация использует операциональную семантику, наблюдаемое поведение конкретной системы можно сравнивать с ожидаемым, потому что такая семантика может быть выполнимой, а может даже использоваться для автоматического генерирования кода. Если используется аксиоматическая семантика, то предусловия и постусловия могут напрямую отобразиться в утверждения в выполнимом коде.
- Верификация
- Когда формальная спецификация подготовлена, её можно использовать для доказательства требуемых свойств. Верификация бывает дедуктивной и модельной: дедуктивная использует автоматическое доказательство теорем или специфические алгебры, а модельная основывает свои выводы не на самой системе, а на построенной по ней модели[4]. При этом модель совершенно не обязательно строить вручную, если применимы оказываются техники вроде en (Program slicing).
Критика формальных методов
Доказательства вручную требуют серьёзных вложений ресурсов и не дают никакой выгоды, кроме подтверждения правильности. В результате формальные методы используются или в тех областях, где доказательства можно получить автоматически программным путём, или в тех, где цена ошибки слишком высока (например, при создании космических аппаратов или магнитно-резонансных томографов).
Абстракции, нотации и языки формальных методов
- [[|en]] (Abstract interpretation)
- Абстрактный автомат (ASM)
- Автомат Бюхи
- [[|en]] (Alloy Analyzer)
- Анализ программного кода и построенных по нему графов:
- [[|en]] (Data-flow analysis) (DFA)
- Анализ потока управления (CFA)
- Динамический анализ кода
- Статический анализ кода
- [[|en]] (B-Method)
- [[|en]] (Vienna Development Method) (VDM, VDM-SL, VDM+)
- [[|en]] (Common Algebraic Specification Language) (CASL) и программа Hets
- Исчисления процессов:
- en (Lustre (programming language))
- Лямбда-исчисление, включая типизированное
- Модель акторов
- Переписывание (TRS)
- [[|en]] (Promela) и верификатор моделей [[|en]] (SPIN model checker)
- en (Rebeca Modeling Language)
- Сети Петри
- [[|en]] (Construction and Analysis of Distributed Processes) (CADP)
- Темпоральная логика (особенно TLA+ и PlusCal)
- [[|en]] (Universal Systems Language) (USL)
- [[|en]] (Esterel)
- [[|en]] (ANSI/ISO C Specification Language) (ACSL) и верификатор Frama-C
- Specification and Description Language (SDL)
- Z-нотация
Примечания
- Jean François Monin, Michael Gerard Hinchey, Understanding formal methods, Springer, 2003, ISBN 1852332476
Литература
Ссылки
- Formal Methods Europe (FME)
- FM — Международный симпозиум по формальным методам, престижная конференция
- ICFEM — Международная конференция по формальным инженерным методам, конференция IEEE ненамного ниже уровнем
- IFM — Международная конференция по интегрированным формальным методам, конференция одного уровня с ICFEM
- Шаблон:Cite web (один из вариантов классификации и большой список средств формальной верификации)
- ↑ Шаблон:Cite web
- ↑ Шаблон:Статья
- ↑ Monin, pp.3-4
- ↑ Верификация программ с помощью моделей Шаблон:Wayback, «Открытые системы» , № 12, 2003.
Шаблон:Выбор языка Шаблон:Software Engineering
