Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

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

Фон [ править ]

Полуформальные методы - это формализмы и языки, которые не считаются полностью « формальными ». Он переносит задачу завершения семантики на более поздний этап, который затем выполняется либо путем интерпретации человеком, либо путем интерпретации с помощью программного обеспечения, такого как генераторы кода или тестовых примеров. [4]

Таксономия [ править ]

Формальные методы могут использоваться на нескольких уровнях:

Уровень 0: Может быть предпринята формальная спецификация , а затем на ее основе неформально разработана программа. Это было названо упрощенными формальными методами . Во многих случаях это может быть наиболее экономичным вариантом.

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

Уровень 2: Средства доказательства теорем могут использоваться для проведения полностью формальных доказательств, проверенных машиной. Это может быть очень дорого и практически оправдано только в том случае, если цена ошибок чрезвычайно высока (например, в критических частях конструкции микропроцессора).

Дополнительная информация об этом раскрыта ниже .

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

  • Денотационная семантика , в которой значение системы выражается в математической теории областей . Сторонники таких методов полагаются на хорошо понятную природу доменов, чтобы придать смысл системе; критики отмечают, что не каждую систему можно интуитивно или естественно рассматривать как функцию.
  • Операционная семантика , в которой значение системы выражается как последовательность действий (предположительно) более простой вычислительной модели. Сторонники таких методов указывают на простоту своих моделей как средство выразительной ясности; критики возражают, что проблема семантики только что отложена (кто определяет семантику более простой модели?).
  • Аксиоматическая семантика , в которой значение системы выражается в терминах предусловий и постусловий, которые выполняются до и после того, как система выполнит задачу, соответственно. Сторонники отмечают связь с классической логикой ; критики отмечают, что такая семантика на самом деле никогда не описывает то, что делает система (только то, что верно до и после).

Легкие формальные методы [ править ]

Некоторые практики считают, что сообщество формальных методов переоценило полную формализацию спецификации или проекта. [5] [6] Они утверждают, что выразительность задействованных языков, а также сложность моделируемых систем делают полную формализацию сложной и дорогостоящей задачей. В качестве альтернативы были предложены различные упрощенные формальные методы, которые подчеркивают частичную спецификацию и целенаправленное применение. Примеры такого легкого подхода к формальным методам включают сплав моделирование объекта обозначение, [7] Синтез Denney в некоторых аспектах Z обозначений с использованием случае приводом развитием, [8]и инструменты CSK VDM . [9]

Использует [ редактировать ]

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

Спецификация [ править ]

Формальные методы могут использоваться для описания разрабатываемой системы на любом желаемом уровне (ах) детализации. Это формальное описание может использоваться для руководства дальнейшими разработками (см. Следующие разделы); кроме того, его можно использовать для проверки того, что требования к разрабатываемой системе были полностью и точно определены, или для формализации требований к системе, выражая их на формальном языке с точным и однозначно определенным синтаксисом и семантикой.

Потребность в формальных системах спецификаций отмечалась годами. В отчете ALGOL 58 [10] Джон Бэкус представил формальную нотацию для описания синтаксиса языка программирования, позже названную нормальной формой Бэкуса, а затем переименованной в форму Бэкуса – Наура (BNF). [11] Бэкус также писал, что формальное описание значения синтаксически корректных программ на Алголе не было завершено вовремя для включения в отчет. «Поэтому формальная трактовка семантики юридических программ будет включена в следующий документ». Так и не появилось.

Развитие [ править ]

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

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

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

Подтверждение [ править ]

Формальная проверка - это использование программных инструментов для доказательства свойств формальной спецификации или для доказательства того, что формальная модель реализации системы удовлетворяет ее спецификации.

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

Подтверждение выхода [ править ]

Подтверждение подписи - это использование формального инструмента проверки, пользующегося большим доверием. Такой инструмент может заменить традиционные методы проверки (инструмент может быть даже сертифицирован).

Доказательство, направленное человеком [ править ]

Иногда мотивацией для доказательства правильности системы является не очевидная потребность в подтверждении правильности системы, а желание лучше понять систему. Следовательно, некоторые доказательства правильности производятся в стиле математических доказательств : рукописные (или набранные) с использованием естественного языка с использованием уровня неформальности, общего для таких доказательств. «Хорошее» доказательство - это такое доказательство, которое читают и понимают другие люди.

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

Автоматическое доказательство [ править ]

Напротив, растет интерес к получению доказательств правильности таких систем с помощью автоматизированных средств. Автоматизированные методы делятся на три основные категории:

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

Некоторым автоматическим средствам доказательства теорем требуется руководство относительно того, какие свойства «достаточно интересны», в то время как другие работают без вмешательства человека. Специалисты по проверке моделей могут быстро увязнуть в проверке миллионов неинтересных состояний, если им не дана достаточно абстрактная модель.

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

Критики отмечают, что некоторые из этих систем подобны оракулам : они заявляют истину, но не объясняют эту истину. Также существует проблема « проверки верификатора »; если программа, которая помогает в проверке, сама по себе не доказана, могут быть основания сомневаться в правильности полученных результатов. Некоторые современные инструменты проверки моделей создают «журнал проверки», в котором подробно описывается каждый этап проверки, что позволяет выполнять независимую проверку при наличии подходящих инструментов.

Основная особенность подхода абстрактной интерпретации заключается в том, что он обеспечивает надежный анализ, т.е. ложноотрицательные результаты не возвращаются. Более того, его можно эффективно масштабировать, настраивая абстрактную область, представляющую свойство, которое нужно проанализировать, и применяя операторы расширения [12], чтобы получить быструю сходимость.

Приложения [ править ]

Формальные методы применяются в различных областях аппаратного и программного обеспечения, включая маршрутизаторы, коммутаторы Ethernet, протоколы маршрутизации, приложения безопасности и микроядра операционной системы, такие как seL4 . Есть несколько примеров, в которых они использовались для проверки функциональности аппаратного и программного обеспечения, используемого в контроллерах домена [ требуется пояснение ] . IBM использовала ACL2 , средство доказательства теорем, в процессе разработки процессоров AMD x86. [ необходима цитата ] Intel использует такие методы для проверки своего оборудования и прошивки (постоянное программное обеспечение, запрограммированное в постоянную память) [ необходима цитата ] .Dansk Datamatik Center использовал формальные методы в 1980-х годах для разработки системы компиляции для языка программирования Ada, которая впоследствии стала долгоживущим коммерческим продуктом. [13] [14]

Есть несколько других проектов НАСА, в которых применяются формальные методы, такие как система воздушного транспорта нового поколения [ необходима цитата ] , интеграция беспилотной системы самолета в национальную систему воздушного пространства [15] и скоординированное разрешение и обнаружение конфликтов с помощью воздушных судов (ACCoRD). [16] B-метод с Atelier B , [17] используется для разработки автоматов безопасности для различных метрополитенов, установленных по всему миру компаниями Alstom и Siemens , а также для сертификации Common Criteria и разработки системных моделей ATMEL и STMicroelectronics..

Формальная проверка часто используется в оборудовании большинства известных поставщиков оборудования, таких как IBM, Intel и AMD. Есть много областей аппаратного обеспечения, в которых Intel использовала FM для проверки работы продуктов, таких как параметризованная проверка согласованного с кешем протокола [18], проверка механизма выполнения процессора Intel Core i7 [19] (с использованием доказательства теорем, BDD , и символьная оценка), оптимизация для архитектуры Intel IA-64 с использованием средства доказательства теорем HOL [20] и проверка высокопроизводительного двухпортового контроллера Gigabit Ethernet с поддержкой протокола PCI Express и усовершенствованной технологии управления Intel с использованием Cadence. [21]Аналогичным образом IBM использовала формальные методы для проверки силовых вентилей, [22] регистров [23] и функциональной проверки микропроцессора IBM Power7. [24]

В разработке программного обеспечения [ править ]

В разработке программного обеспечения формальные методы - это математические подходы к решению программных (и аппаратных) проблем на уровнях требований, спецификаций и проектирования. Формальные методы, скорее всего, будут применяться к критически важному для безопасности или критически важному для безопасности программному обеспечению и системам, таким как программное обеспечение авионики . Стандарты обеспечения безопасности программного обеспечения, такие как DO-178C, допускают использование формальных методов посредством дополнений, а Common Criteria предписывает формальные методы на самых высоких уровнях категоризации.

Для последовательного программного обеспечения примеры формальных методов включают B-метод , языки спецификации, используемые в автоматическом доказательстве теорем , RAISE и Z-нотацию .

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

Язык объектных ограничений (и такие специализации, как язык моделирования Java ) позволил формально определять объектно-ориентированные системы, если не обязательно формально подтверждать их.

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

Другой подход к формальным методам в разработке программного обеспечения - это написать спецификацию в некоторой форме логики - обычно это вариант логики первого порядка (FOL) - а затем напрямую выполнять логику, как если бы это была программа. OWL язык, основанный на Описание Logic (DL), является примером. Также ведется работа по автоматическому отображению некоторой версии английского (или другого естественного языка) на логику и обратно, а также прямое выполнение логики. Примеры: английский, контролируемый попытками.и Internet Business Logic, которые не стремятся контролировать словарный запас или синтаксис. Особенностью систем, поддерживающих двунаправленное отображение логики на английском языке и прямое выполнение логики, является то, что их можно заставить объяснять свои результаты на английском языке на деловом или научном уровне. [ необходима цитата ]

Формальные методы и обозначения [ править ]

Доступно множество формальных методов и обозначений.

Языки спецификации [ править ]

  • Абстрактные государственные машины (ASM)
  • Вычислительная логика для аппликативного Common Lisp (ACL2)
  • Актерская модель
  • Сплав
  • Язык спецификаций ANSI / ISO C (ACSL)
  • Язык спецификации автономной системы (ASSL)
  • B-метод
  • CADP
  • Общий язык алгебраической спецификации (CASL)
  • Эстерель
  • Язык моделирования Java (JML)
  • Помощник по программному обеспечению, основанный на знаниях (KBSA)
  • Блеск
  • mCRL2
  • Идеальный разработчик
  • Сети Петри
  • Предикативное программирование
  • Расчет процесса
    • CSP
    • LOTOS
    • π-исчисление
  • ПОДНИМАТЬ
  • Язык моделирования Ребека
  • СПАРК Ада
  • Spec Sharp (Spec #)
  • Спецификация и язык описания
  • TLA +
  • USL
  • VDM
    • VDM-SL
    • VDM ++
  • Обозначение Z

Проверка моделей [ править ]

Основная статья: Список инструментов проверки модели
  • ESBMC [25]
  • MALPAS Software Static Analysis Toolset - средство проверки промышленных моделей, используемое для формального подтверждения критически важных для безопасности систем.
  • PAT - бесплатная программа проверки модели, симулятора и средства проверки уточнения для параллельных систем и расширений CSP (например, общих переменных, массивов, справедливости)
  • ВРАЩЕНИЕ
  • UPPAAL

Организации [ править ]

Главная: Категория: Организации формальными методами
  • APCB
  • BCS-FACS
  • Формальные методы Европа
  • Группа пользователей Z

См. Также [ править ]

  • Абстрактная интерпретация
  • Автоматическое доказательство теорем
  • Дизайн по контракту
  • Формальные методы люди
  • Формальная спецификация
  • Формальная проверка
  • Формальная система
  • Проверка модели
  • Программная инженерия
  • Язык спецификации

Ссылки [ править ]

  1. ^ Батлер, RW (2001-08-06). "Что такое формальные методы?" . Проверено 16 ноября 2006 .
  2. ^ Холлоуэй, С. Майкл. «Почему инженерам следует рассматривать формальные методы» (PDF) . 16-я конференция по системам цифровой авионики (27–30 октября 1997 г.). Архивировано из оригинального (PDF) 16 ноября 2006 года . Проверено 16 ноября 2006 . Cite journal requires |journal= (help)
  3. ^ Монин, pp.3-4
  4. ^ X2R-2, отчет D5.1 .
  5. ↑ Дэниел Джексон и Жаннетт Винг , «Легкие формальные методы» , IEEE Computer , апрель 1996 г.
  6. ^ Вину Джордж и Рэйфорд Вон, «Применение облегченных формальных методов в разработке требований». Архивировано 01марта 2006 г.на Wayback Machine , Crosstalk: The Journal of Defense Software Engineering , январь 2003 г.
  7. ^ Дэниел Джексон, «Сплав: легкая нотация моделирования объектов» , ACM Transactions по разработке программного обеспечения и методологии (TOSEM) , том 11, выпуск 2 (апрель 2002 г.), стр. 256-290
  8. ^ Ричард Денни, Успех с использованием примеров: работа с умом для обеспечения качества , Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6 . 
  9. ^ Стен Agerholm и Питер Г. Ларсен, «облегченный подход к формальным методам» Архивированные 2006-03-09 на Wayback Machine , в Трудах Международного семинара по текущим тенденциям в прикладных формальных методах , Боппард, Германия, Springer-Verlag, Октябрь 1998
  10. Перейти ↑ Backus, JW (1959). "Синтаксис и семантика предлагаемого международного алгебраического языка Цюрихской конференции ACM-GAMM". Материалы Международной конференции по обработке информации . ЮНЕСКО.
  11. ^ Кнут, Дональд Э. (1964), Нормальная форма Бэкуса против формы Бэкуса Наура. Сообщения ACM , 7 (12): 735–736.
  12. ^ А. Кортеси и М. Заниоли, Расширяющие и сужающие операторы для абстрактной интерпретации . Компьютерные языки, системы и структуры. Том 37 (1), стр. 24–42, Elsevier, ISSN 1477-8424 (2011). 
  13. ^ Bjørner, Dines; Грамм, Кристиан; Oest, Ole N .; Rystrøm, Лейф (2011). "Данск Датаматик Центр". В Impagliazzo, Джон; Лундин, Пер; Wangler, Benkt (ред.). История Nordic Computing 3: Достижения IFIP в области информационных и коммуникационных технологий . Springer. С. 350–359.
  14. ^ Bjørner, Dines; Хавелунд, Клаус. «40 лет формальных методов: некоторые препятствия и некоторые возможности?». FM 2014: формальные методы: 19-й международный симпозиум, Сингапур, 12–16 мая 2014 г. Материалы (PDF) . Springer. С. 42–61.
  15. Перейти ↑ Gheorghe, AV, & Ancel, E. (2008, ноябрь). Интеграция беспилотных авиационных систем в Национальную систему воздушного пространства. В области «Инфраструктурные системы и услуги: построение сетей для более светлого будущего» (ИНФРА), Первая международная конференция 2008 г. (стр. 1-5). IEEE.
  16. ^ Скоординированное разрешение и обнаружение конфликтов в воздухе, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/
  17. ^ "Ателье B" . www.atelierb.eu .
  18. ^ CT Chou, PK Mannava, S. Park, « Простой метод параметризованной проверки протоколов согласованности кэша », Формальные методы в автоматизированном проектировании, стр. 382–398, 2004.
  19. ^ Formal Verification in Intel® Core ™ i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371 , по состоянию на 13 сентября 2013 г.
  20. ^ Дж. Гранди, «Проверенные оптимизации для архитектуры Intel IA-64», Доказательство теорем в логике высокого порядка, Springer Berlin Heidelberg, 2004, стр. 215–232.
  21. ^ Э. Селигман, И. Яром, « Наиболее известные методы использования Cadence Conformal LEC », в Intel.
  22. ^ С. Эйснер, А. Нахир, К. Yorav, « Функциональная проверка мощности закрытого типа конструкций от композиционного рассуждения », Computer Aided Verification, Springer Berlin Heidelberg, стр. 433-445.
  23. ^ PC Атти, Х. Чоклер, « Автоматическая проверка отказоустойчивых эмуляций регистров », Электронные заметки по теоретической информатике, вып. 149, нет. 1. С. 49–60.
  24. ^ KD Schubert, W. Roesner, JM Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, « Функциональная проверка микропроцессора IBM POWER7 и многопроцессорных систем POWER7 », IBM Journal of Research and Development, vol. 55, № 3.
  25. ^ "ESBMC" . esbmc.org .
  • Эта статья основана на материалах, взятых из Free On-line Dictionary of Computing до 1 ноября 2008 г. и включенных в соответствии с условиями «перелицензирования» GFDL версии 1.3 или новее.

Дальнейшее чтение [ править ]

  • Джонатан П. Боуэн и Майкл Г. Хинчи, Формальные методы . В книге Аллена Б. Такера-младшего (ред.), Справочник по компьютерным наукам , 2-е издание, раздел XI, Разработка программного обеспечения , глава 106, страницы 106-1 - 106-25, Chapman & Hall / CRC Press , Association for Computing Machinery , 2004 г.
  • Юбер Гаравель (редактор) и Сюзанна Граф. Формальные методы безопасных и защищенных компьютерных систем . Bundesamt für Sicherheit in der Informationstechnik , исследование BSI 875, Бонн, Германия, декабрь 2013 г.
  • Гаравель, Юбер; тер Бик, Морис Х .; ван де Поль, Хако (29 августа 2020 г.). «Экспертный обзор формальных методов 2020 года». Формальные методы для промышленных критических систем . Конспект лекций по информатике (LNCS). 12327 . Springer . С. 3–69. DOI : 10.1007 / 978-3-030-58298-2_1 . ISBN 978-3-030-58297-5.* Майкл Г. Хинчи, Джонатан П. Боуэн и Эмиль Вассев, Формальные методы . В книге Филипа А. Лапланте (ред.), Энциклопедия программной инженерии , Тейлор и Фрэнсис , 2010 г., страницы 308–320.
  • Марике Хейсман, Дилиан Гуров и Александр Малкис, Формальные методы: от академических кругов к производственной практике - Путеводитель , arXiv: 2002.07279, 2020.
  • Глейршер, Марио; Мармсолер, Диего (9 сентября 2020 г.). «Формальные методы в проектировании надежных систем: опрос профессионалов из Европы и Северной Америки» . Эмпирическая программная инженерия . Springer Nature . 25 : 4473–4546. DOI : 10.1007 / s10664-020-09836-5 .
  • Жан Франсуа Монен и Майкл Г. Хинчи , Понимание формальных методов , Springer , 2003, ISBN 1-85233-247-6 . 

Внешние ссылки [ править ]

  • Формальные методы в Европе (FME)
  • Формальные методы вики
  • Формальные методы от Foldoc
Архивные материалы
  • Ключевое слово формального метода в Microsoft Academic Search через Archive.org
  • Свидетельства об использовании и влиянии формальных методов на промышленность при поддержке проекта DEPLOY (EU FP7) на Archive.org