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

Из Википедии, бесплатной энциклопедии

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

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

Предыстория [ править ]

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

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

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

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

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

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

формальные методы Облегченные ​

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

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

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

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

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

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

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

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

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

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

Проверка [ править ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Модельные шашки [ править ]

Основная статья: Список инструментов проверки моделей

и соревнования Решатели ​

Многие задачи формальных методов являются NP-трудными , но могут быть решены в случаях, возникающих на практике. Например, булева проблема выполнимости является NP-полной по теореме Кука – Левина , но решатели SAT могут решать множество больших задач. Существуют «решатели» множества задач, возникающих при использовании формальных методов, и периодически проводится множество соревнований по оценке современного состояния решения таких задач. [26]

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

Основная статья: Категория: Организации формальных методов

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

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

  1. ^ Батлер, RW (6 августа 2001 г.). «Что такое формальные методы?» . Проверено 16 ноября 2006 г.
  2. ^ Холлоуэй, К. Майкл. «Почему инженерам следует использовать формальные методы» (PDF) . 16-я конференция по системам цифровой авионики (27–30 октября 1997 г.). Архивировано из оригинала (PDF) 16 ноября 2006 года . Проверено 16 ноября 2006 г. {{cite journal}}: Для цитирования журнала требуется |journal= ( помощь )
  3. ^ Монин, стр.3-4.
  4. ^ X2R-2, поставка D5.1 .
  5. ^ Дэниел Джексон и Жаннетт Винг , «Облегченные формальные методы» , IEEE Computer , апрель 1996 г.
  6. ^ Вину Джордж и Рэйфорд Вон, «Применение облегченных формальных методов в разработке требований». Архивировано 1 марта 2006 г. в Wayback Machine , Crosstalk: Журнал оборонной разработки программного обеспечения , январь 2003 г.
  7. ^ Дэниел Джексон, «Сплав: облегченная нотация моделирования объектов» , Транзакции ACM по разработке программного обеспечения и методологии (TOSEM) , Том 11, Выпуск 2 (апрель 2002 г.), стр. 256-290
  8. ^ Ричард Денни, Успех в сценариях использования: разумная работа для обеспечения качества , Addison-Wesley Professional Publishing, 2005, ISBN   0-321-31643-6 .
  9. ^ Стен Агерхольм и Питер Г. Ларсен, «Облегченный подход к формальным методам». Архивировано 9 марта 2006 г. в Wayback Machine , В материалах международного семинара по текущим тенденциям в прикладных формальных методах , Боппард, Германия, Springer-Verlag, октябрь 1998 г.
  10. ^ Бэкус, JW (1959). «Синтаксис и семантика предложенного международного алгебраического языка на Цюрихской конференции ACM-GAMM». Материалы международной конференции по обработке информации . ЮНЕСКО.
  11. ^ Кнут, Дональд Э. (1964), Нормальная форма Бэкуса против формы Бэкуса Наура. Сообщения ACM , 7(12):735–736.
  12. ^ А. Кортези и М. Заниоли, Операторы расширения и сужения для абстрактной интерпретации . Компьютерные языки, системы и структуры. Том 37 (1), стр. 24–42, Elsevier, ISSN   1477-8424 (2011).
  13. ^ Бьёрнер, Дайнс; Грэм, Кристиан; Оест, Оле Н.; Ристрем, Лейф (2011). «Датский компьютерный центр». В Импальяццо, Джон; Лундин, Пер; Ванглер, Бенкт (ред.). История Nordic Computing 3: Достижения ИФИП в области информационных и коммуникационных технологий . Спрингер. стр. 350–359.
  14. ^ Бьёрнер, Дайнс; Хавелунд, Клаус. «40 лет формальных методов: некоторые препятствия и некоторые возможности?». FM 2014: Формальные методы: 19-й Международный симпозиум, Сингапур, 12–16 мая 2014 г. Материалы (PDF) . Спрингер. стр. 42–61.
  15. ^ Георге, А.В., и Ансель, Э. (2008, ноябрь). Интеграция беспилотных авиационных систем в Национальную систему воздушного пространства. В книге «Инфраструктурные системы и услуги: построение сетей для светлого будущего» (INFRA), Первая международная конференция 2008 г. (стр. 1–5). IEEE.
  16. ^ Скоординированное разрешение и обнаружение конфликтов с помощью самолетов, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/. Архивировано 5 марта 2016 г. в Wayback Machine.
  17. ^ «Ателье Б» . www.atelierb.eu .
  18. ^ CT Chou, PK Mannava, S. Park, « Простой метод параметризованной проверки протоколов когерентности кэша », Формальные методы в автоматизированном проектировании, стр. 382–398, 2004.
  19. ^ Формальная проверка в механизме выполнения процессора Intel Core i7, http://cps-vo.org/node/1371. Архивировано 3 мая 2015 г. на Wayback Machine , по состоянию на 13 сентября 2013 г.
  20. ^ Дж. Гранди, «Проверенная оптимизация для архитектуры Intel IA-64», В «Доказательстве теорем в логике высшего порядка», Springer Berlin Heidelberg, 2004, стр. 215–232.
  21. ^ Э. Селигман, И. Яром, « Наиболее известные методы использования Cadence Conformal LEC », в Intel.
  22. ^ К. Эйснер, А. Нахир, К. Йорав, « Функциональная проверка конструкций с силовым затвором с помощью композиционных рассуждений». [ постоянная мертвая ссылка ] «, Компьютерная проверка, Springer Berlin Heidelberg, стр. 433–445.
  23. ^ ПК Атти, Х. Чоклер, « Автоматическая проверка отказоустойчивых эмуляций регистров », Электронные заметки в теоретической информатике, том. 149, нет. 1, стр. 49–60.
  24. ^ К.Д. Шуберт, В. Рознер, Дж. М. Ладден, Дж. Джексон, Дж. Бухерт, В. Парути, Б. Брок, « Функциональная проверка микропроцессора IBM POWER7 и многопроцессорных систем POWER7 », IBM Journal of Research and Development, vol. 55, № 3.
  25. ^ «ЭСБМК» . esbmc.org .
  26. ^ Барточчи, Эцио; Бейер, Дирк; Блэк, Пол Э.; Федюкович, Григорий; Гаравель, Юбер; Хартманс, Арнд; Хейсман, Марике; Кордон, Фабрис; Нагеле, Джулиан; Сигиряну, Михаэла; Штеффен, Бернхард; Суда, Мартин; Сатклифф, Джефф; Вебер, Тьярк; Ямада, Акихиса (2019). Бейер, Дирк; Хейсман, Марике; Кордон, Фабрис; Штеффен, Бернхард (ред.). «TOOLympics 2019: Обзор соревнований по формальным методам» . Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. Чам: Springer International Publishing: 3–24. дои : 10.1007/978-3-030-17502-3_1 . ISBN  978-3-030-17502-3 .
  27. ^ Фролейкс, Нильс; Хойле, Марин; Изер, Маркус; Ярвисало, Матти; Суда, Мартин (01 декабря 2021 г.). «Конкурс САТ 2020» . Искусственный интеллект . 301 : 103572. doi : 10.1016/j.artint.2021.103572 . ISSN   0004-3702 .
  28. ^ Корнехо, Сезар (27 января 2021 г.). «Арифметическая поддержка сплавов на основе SAT» . Материалы 35-й Международной конференции IEEE/ACM по автоматизированной разработке программного обеспечения . АСЭ '20. Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники: 1161–1163. дои : 10.1145/3324884.3415285 . ISBN  978-1-4503-6768-4 .
  29. ^ Барретт, Кларк; Детерс, Морган; де Моура, Леонардо; Оливерас, Альберт; Стамп, Аарон (01 марта 2013 г.). «6 лет СМТ-КОМП» . Журнал автоматизированного рассуждения . 50 (3): 243–277. дои : 10.1007/s10817-012-9246-5 . ISSN   1573-0670 .
  30. ^ Федюкович, Григорий; Рюммер, Филипп (13 сентября 2021 г.). «Отчет о конкурсе: CHC-COMP-21» . Электронные труды по теоретической информатике . 344 : 91–108. arXiv : 2008.02939 . дои : 10.4204/EPTCS.344.7 . ISSN   2075-2180 .
  31. ^ Шукла, Анкит; Бьер, Армин; Пулина, Лука; Зайдль, Мартина (ноябрь 2019 г.). «Обзор применения количественных логических формул» . ИИЭР: 78–84. дои : 10.1109/ICTAI.2019.00020 . ISBN  978-1-7281-3798-8 . {{cite journal}}: Для цитирования журнала требуется |journal= ( помощь )
  32. ^ Пулина, Лука; Зайдль, Мартина (01 сентября 2019 г.). «Оценки решателей QBF 2016 и 2017 годов (QBFEVAL'16 и QBFEVAL'17)» . Искусственный интеллект . 274 : 224–248. дои : 10.1016/j.artint.2019.04.002 . ISSN   0004-3702 .
  33. ^ Бейер, Дирк (2022). Фисман, Дана; Розу, Григоре (ред.). «Ход проверки программного обеспечения: SV-COMP 2022» . Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. Чам: Springer International Publishing: 375–402. дои : 10.1007/978-3-030-99527-0_20 . ISBN  978-3-030-99527-0 .
  34. ^ Алур, Раджив; Фисман, Дана; Сингх, Ришаб; Солар-Лезама, Армандо (28 ноября 2017 г.). «СиГуС-Комп 2017: Итоги и анализ» . Электронные труды по теоретической информатике . 260 : 97–115. arXiv : 1611.07627 . дои : 10.4204/EPTCS.260.9 . ISSN   2075-2180 .

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

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

Архивный материал
Retrieved from "https://en.wikipedia.org/w/index.php?title=Formal_methods&oldid=1220689780"