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

kassidy
  • 2020-05-28
  • 2

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Примечания

  • Jean François Monin, Michael Gerard Hinchey, Understanding formal methods , Springer, 2003, ISBN 1852332476
  1. R. W. Butler. (6 августа 2001). Дата обращения: 16 ноября 2006. 25 августа 2012 года.
  2. C. Michael Holloway. (неопр.) . — 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). . 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 : . ISBN 9781450394666 .

Ссылки

  • (FME)
  • — , престижная конференция
  • — , конференция IEEE ненамного ниже уровнем
  • — , конференция одного уровня с ICFEM
  • Sophie Lathouwers, Vadim Zaytsev. (англ.) . (один из вариантов классификации и большой список средств формальной верификации)
Источник —

kassidy
  • 2020-05-28
  • 2
  • Tags:

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

The title for the last searches