stringtranslate.com

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

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

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

Фон

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

Таксономия

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

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

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

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

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

Использование

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

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

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

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

Разработка

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

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

Проверка

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

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

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

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

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

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

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

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

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

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

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

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

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

Приложения

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

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

Формальная проверка часто используется в оборудовании большинством известных поставщиков оборудования, таких как IBM, Intel и AMD. Существует много областей аппаратного обеспечения, где Intel использовала формальные методы для проверки работы продуктов, такие как параметризованная проверка протокола когерентности кэша, [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, допускают использование формальных методов путем дополнения, а Общие критерии требуют формальных методов на самых высоких уровнях категоризации.

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

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

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

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

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

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

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

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

Модельные шашки

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

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

Организации

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

Рекомендации

  1. ^ Батлер, RW (06 августа 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/
  17. ^ "Ателье Б". www.atelierb.eu .
  18. ^ CT Chou, PK Mannava, S. Park, «Простой метод параметризованной проверки протоколов когерентности кэша», Формальные методы в компьютерном проектировании, стр. 382–398, 2004.
  19. ^ Формальная проверка в механизме выполнения процессора Intel® Core™ i7, http://cps-vo.org/node/1371, по состоянию на 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. doi : 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.

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

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

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