stringtranslate.com

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

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

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

Использует

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

Спецификация

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

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

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

Синтез

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

Проверка

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

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

Проверка подписи

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

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

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

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

Автоматизированное доказательство

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

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

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

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

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

Методы

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

Языки спецификации

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

Диаграммы бинарных решений

Бинарная диаграмма решений — это структура данных, которая представляет собой булеву функцию . [11] Если булева формула выражает, что выполнение программы соответствует спецификации, бинарная диаграмма решений может быть использована для определения того, является ли она тавтологией; то есть всегда ли она оценивается как ИСТИНА. Если это так, то программа всегда соответствует спецификации. [12]

Решатели SAT

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

Приложения

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

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

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

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

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

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

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

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

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

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

Полуформальные методы

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

Некоторые специалисты считают, что сообщество формальных методов переоценило полную формализацию спецификации или проекта. [27] [28] Они утверждают, что выразительность задействованных языков, а также сложность моделируемых систем делают полную формализацию сложной и дорогостоящей задачей. В качестве альтернативы были предложены различные легкие формальные методы, которые подчеркивают частичную спецификацию и целенаправленное применение. Примерами такого легкого подхода к формальным методам являются нотация моделирования объектов Alloy , [29] синтез Денни некоторых аспектов нотации Z с разработкой, основанной на вариантах использования , [30] и инструменты CSK VDM . [31]

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

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

Языки спецификации

Модели проверки

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

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

Организации

Смотрите также

Ссылки

  1. ^ Батлер, Р. У. (2001-08-06). "Что такое формальные методы?" . Получено 16 ноября 2006 г.
  2. ^ Холлоуэй, К. Майкл. «Почему инженеры должны учитывать формальные методы» (PDF) . 16-я конференция по цифровым авиационным системам (27–30 октября 1997 г.). Архивировано из оригинала (PDF) 16 ноября 2006 г. Получено 16 ноября 2006 г. {{cite journal}}: Цитировать журнал требует |journal=( помощь )
  3. ^ Монин, стр.3-4
  4. ^ Utting, Mark; Reeves, Steve (31 августа 2001 г.). «Обучение формальным методам lite через тестирование». Software Testing, Verification and Reliability . 11 (3): 181–195. doi :10.1002/stvr.223.
  5. ^ Бэкус, Дж. В. (1959). «Синтаксис и семантика предлагаемого международного алгебраического языка Цюрихской конференции ACM-GAMM». Труды Международной конференции по обработке информации . ЮНЕСКО.
  6. ^ Кнут, Дональд Э. (1964), Нормальная форма Бэкуса против формы Бэкуса-Наура. Сообщения ACM , 7(12):735–736.
  7. ^ О'Херн, Питер У.; Теннент, Роберт Д. (1997). Языки, подобные Алголу .
  8. ^ Гулвани, Сумит; Полозов, Александр; Сингх, Ришабх (2017). «Синтез программ». Основы и тенденции в языках программирования . 4 (1–2): 1–119. doi :10.1561/2500000010.
  9. ^ А. Кортези и М. Заниоли, Операторы расширения и сужения для абстрактной интерпретации. Компьютерные языки, системы и структуры. Том 37(1), стр. 24–42, Elsevier, ISSN  1477-8424 (2011).
  10. ^ Бьёрнер, Дайнес; Хенсон, Мартин К. (2008). Логика языков спецификаций . С. VII–XI.
  11. ^ Брайант, Рэндал Э. (2018). «Диаграммы бинарных решений». В Кларке, Эдмунд М.; Хензингер, Томас А.; Вайт, Хельмут; Блум, Родерик (ред.). Справочник по проверке моделей . стр. 191.
  12. ^ Чаки, Сагар; Гурфинкель, Ари (2018). «Проверка символической модели на основе BDD». В Кларке, Эдмунд М.; Хензингер, Томас А.; Вайт, Хельмут; Блум, Родерик (ред.). Справочник по проверке моделей . стр. 191.
  13. ^ Прасад, Мукул Р.; Бире, Армин; Гупта, Аарти (25 января 2005 г.). «Обзор последних достижений в области формальной верификации на основе SAT». Международный журнал по программным средствам для передачи технологий . 7 (2): 156–173. doi :10.1007/s10009-004-0183-4.
  14. ^ Бьёрнер, Дайнс; Грэм, Кристиан; Оест, Оле Н.; Ристрем, Лейф (2011). «Данский Датаматик Центр». В Импальяццо, Джон; Лундин, Пер; Ванглер, Бенкт (ред.). История Nordic Computing 3: Достижения ИФИП в области информационных и коммуникационных технологий . Спрингер. стр. 350–359.
  15. ^ Бьёрнер, Дайнес; Хавелунд, Клаус. «40 лет формальных методов: некоторые препятствия и некоторые возможности?». FM 2014: Формальные методы: 19-й международный симпозиум, Сингапур, 12–16 мая 2014 г. Труды (PDF) . Springer. стр. 42–61.
  16. ^ Gheorghe, AV, & Ancel, E. (2008, ноябрь). Интеграция беспилотных авиационных систем в национальную систему воздушного пространства. В Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (стр. 1-5). IEEE.
  17. ^ Координированное разрешение и обнаружение конфликтов с воздуха, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ Архивировано 05.03.2016 на Wayback Machine
  18. ^ "Ателье Б". www.atelierb.eu .
  19. ^ CT Chou, PK Mannava, S. Park, «Простой метод параметризованной проверки протоколов когерентности кэша», Formal Methods in Computer-Aided Design, стр. 382–398, 2004.
  20. ^ Формальная проверка в Intel Core i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371 Архивировано 03.05.2015 на Wayback Machine , доступ получен 13 сентября 2013 г.
  21. ^ Дж. Гранди, «Проверенные оптимизации для архитектуры Intel IA-64», в книге «Доказательство теорем в логике высшего порядка», Springer Berlin Heidelberg, 2004, стр. 215–232.
  22. ^ Э. Селигман, И. Яром, «Наиболее известные методы использования Cadence Conformal LEC», на сайте Intel.
  23. ^ C. Eisner, A. Nahir, K. Yorav, «Функциональная проверка конструкций с силовыми вентилями с помощью композиционных рассуждений [ постоянная мертвая ссылка ] », Computer Aided Verification, Springer Berlin Heidelberg, стр. 433–445.
  24. ^ П. К. Этти, Х. Чоклер, «Автоматическая проверка отказоустойчивых эмуляций регистров», Electronic Notes in Theoretical Computer Science, т. 149, № 1, стр. 49–60.
  25. ^ К. Д. Шуберт, В. Реснер, Дж. М. Ладден, Дж. Джексон, Дж. Бухерт, В. Парути, Б. Брок, «Функциональная проверка микропроцессора IBM POWER7 и многопроцессорных систем POWER7», IBM Journal of Research and Development, т. 55, № 3.
  26. ^ X2R-2, результат D5.1 .
  27. ↑ Дэниел Джексон и Жанетт Винг , «Облегченные формальные методы», IEEE Computer , апрель 1996 г.
  28. ^ Вину Джордж и Рэйфорд Вон, «Применение облегченных формальных методов в разработке требований». Архивировано 1 марта 2006 г. в Wayback Machine , Crosstalk: The Journal of Defense Software Engineering , январь 2003 г.
  29. ^ Дэниел Джексон, «Alloy: облегченная нотация объектного моделирования», ACM Transactions on Software Engineering and Methodology (TOSEM) , том 11, выпуск 2 (апрель 2002 г.), стр. 256-290
  30. ^ Ричард Денни, Успех в вариантах использования: разумная работа для обеспечения качества , Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6 . 
  31. ^ Стен Агерхольм и Питер Г. Ларсен, «Облегченный подход к формальным методам», архив 2006-03-09 в Wayback Machine , в трудах Международного семинара по современным тенденциям в прикладных формальных методах , Боппард, Германия, Springer-Verlag, октябрь 1998 г.
  32. ^ "ESBMC". esbmc.org .
  33. ^ Барточчи, Эцио; Бейер, Дирк; Блэк, Пол Э.; Федюкович, Григорий; Гаравел, Хуберт; Хартманнс, Арнд; Хейсман, Марике; Кордон, Фабрис; Нагеле, Джулиан; Сигиреану, Михаэла; Штеффен, Бернхард; Суда, Мартин; Сатклифф, Джефф; Вебер, Тьярк; Ямада, Акихиса (2019). «TOOLympics 2019: Обзор соревнований по формальным методам». В Бейер, Дирк; Хейсман, Марике; Кордон, Фабрис; Штеффен, Бернхард (ред.). Инструменты и алгоритмы для построения и анализа систем . Конспект лекций по информатике. Cham: Springer International Publishing. стр. 3–24. дои : 10.1007/978-3-030-17502-3_1 . ISBN 978-3-030-17502-3.
  34. ^ Фролейкс, Нильс; Хойле, Марин; Изер, Маркус; Ярвисало, Матти; Суда, Мартин (01 декабря 2021 г.). «Конкурс САТ 2020». Искусственный интеллект . 301 : 103572. doi : 10.1016/j.artint.2021.103572 . ISSN  0004-3702.
  35. ^ Корнехо, Сезар (2021-01-27). «SAT-based arithmetic support for solid». Труды 35-й Международной конференции IEEE/ACM по автоматизированной программной инженерии . ASE '20. Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. стр. 1161–1163. doi :10.1145/3324884.3415285. ISBN 978-1-4503-6768-4.
  36. ^ Барретт, Кларк; Детерс, Морган; де Моура, Леонардо; Оливерас, Альберт; Стамп, Аарон (2013-03-01). «6 лет SMT-COMP». Журнал автоматизированного рассуждения . 50 (3): 243–277. doi :10.1007/s10817-012-9246-5. ISSN  1573-0670.
  37. ^ Федюкович, Григорий; Рюммер, Филипп (2021-09-13). «Отчет о конкурсе: CHC-COMP-21». Электронные труды по теоретической информатике . 344 : 91–108. arXiv : 2008.02939 . doi : 10.4204/EPTCS.344.7 . ISSN  2075-2180.
  38. ^ Шукла, Анкит; Бире, Армин; Пулина, Лука; Зайдл, Мартина (ноябрь 2019 г.). «Обзор приложений квантифицированных булевых формул». 2019 IEEE 31-я Международная конференция по инструментам с искусственным интеллектом (ICTAI) . IEEE. стр. 78–84. doi :10.1109/ICTAI.2019.00020. ISBN 978-1-7281-3798-8.
  39. ^ Пулина, Лука; Зайдль, Мартина (01 сентября 2019 г.). «Оценки решателей QBF 2016 и 2017 годов (QBFEVAL'16 и QBFEVAL'17)». Искусственный интеллект . 274 : 224–248. дои : 10.1016/j.artint.2019.04.002 . ISSN  0004-3702.
  40. ^ Бейер, Дирк (2022). «Прогресс в области проверки программного обеспечения: SV-COMP 2022». В Фисман, Дана; Росу, Григоре (ред.). Инструменты и алгоритмы для построения и анализа систем . Конспект лекций по информатике. Том 13244. Чам: Springer International Publishing. стр. 375–402. doi : 10.1007/978-3-030-99527-0_20 . ISBN 978-3-030-99527-0.
  41. ^ Алур, Раджив; Фисман, Дана; Сингх, Ришабх; Солар-Лезама, Армандо (2017-11-28). "SyGuS-Comp 2017: Результаты и Анализ". Электронные труды по теоретической информатике . 260 : 97–115. arXiv : 1611.07627 . doi : 10.4204/EPTCS.260.9 . ISSN  2075-2180.

Дальнейшее чтение

Внешние ссылки

Архивные материалы