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

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

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

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

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

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

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

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

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

Синтез

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

Проверка

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Техники

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

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

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

Бинарные диаграммы решений

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

Решатели SAT

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

Приложения

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ЭСБМК ^[32]
Набор инструментов для статического анализа программного обеспечения MALPAS — средство проверки моделей промышленного уровня, используемое для формального подтверждения критически важных для безопасности систем.
PAT — бесплатная программа проверки моделей, симулятор и проверка уточнений для параллельных систем и расширений CSP (например, общие переменные, массивы, справедливость)
ВРАЩАТЬСЯ
УПААЛ

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

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

Соревнования SAT — это ежегодные соревнования, в которых сравниваются решатели SAT. ^[34] Решатели SAT используются в инструментах формальных методов, таких как Alloy . ^[35]
CASC — это ежегодный конкурс автоматизированных средств доказательства теорем .
SMT-COMP — ежегодное соревнование решателей SMT , которые применяются для формальной верификации . ^[36]
CHC-COMP — это ежегодное соревнование решателей ограниченных предложений Хорна , которые применяются к формальной проверке. ^[37]
QBFEVAL – это конкурс, проводимый раз в два года среди решателей истинных количественных булевых формул , которые можно применять для проверки моделей . ^[38]^[39]
SV-COMP — это ежегодный конкурс инструментов проверки программного обеспечения. ^[40]
СыГуС-КОМП — ежегодный конкурс средств синтеза программ . ^[41]

Организации

См. также

Ссылки

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

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

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

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

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

Ключевое слово формального метода в Microsoft Academic Search через Archive.org
Доказательства использования формальных методов и их влияния на промышленность, поддержанные DEPLOY. Архивировано 8 июня 2012 г. в проекте Wayback Machine (EU FP7) на Archive.org.

[butler-1] Батлер, RW (6 августа 2001 г.). «Что такое формальные методы?» . Проверено 16 ноября 2006 г.

[2] Холлоуэй, К. Майкл. «Почему инженерам следует использовать формальные методы» (PDF) . 16-я конференция по системам цифровой авионики (27–30 октября 1997 г.). Архивировано из оригинала (PDF) 16 ноября 2006 года . Проверено 16 ноября 2006 г. {{cite journal}}: Для цитирования журнала требуется |journal= ( помощь )

[3] Монин, стр.3-4.

[4] Уттинг, Марк; Ривз, Стив (31 августа 2001 г.). «Облегченное обучение формальным методам посредством тестирования» . Тестирование, проверка и надежность программного обеспечения . 11 (3): 181–195. дои : 10.1002/stvr.223 .

[5] Бэкус, JW (1959). «Синтаксис и семантика предложенного международного алгебраического языка на Цюрихской конференции ACM-GAMM». Материалы международной конференции по обработке информации . ЮНЕСКО.

[6] Кнут, Дональд Э. (1964), Нормальная форма Бэкуса против формы Бэкуса Наура. Сообщения ACM , 7(12):735–736.

[7] О'Хирн, Питер В.; Теннент, Роберт Д. (1997). Алголоподобные языки .

[8] Гулвани, Сумит; Полозов, Александр; Сингх, Ришаб (2017). «Синтез программы» . Основы и тенденции в языках программирования . 4 (1–2): 1–119. дои : 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. дои : 10.1007/s10009-004-0183-4 .

[14] Бьёрнер, Дайнс; Грэм, Кристиан; Оест, Оле Н.; Ристрем, Лейф (2011). «Данский Датаматик Центр». В Импальяццо, Джон; Лундин, Пер; Ванглер, Бенкт (ред.). История Nordic Computing 3: Достижения ИФИП в области информационных и коммуникационных технологий . Спрингер. стр. 350–359.

[15] Бьёрнер, Дайнс; Хавелунд, Клаус. «40 лет формальных методов: некоторые препятствия и некоторые возможности?». FM 2014: Формальные методы: 19-й Международный симпозиум, Сингапур, 12–16 мая 2014 г. Материалы (PDF) . Спрингер. стр. 42–61.

[16] Георге, А.В., и Ансель, Э. (2008, ноябрь). Интеграция беспилотных авиационных систем в Национальную систему воздушного пространства. В книге «Инфраструктурные системы и услуги: построение сетей для светлого будущего» (INFRA), Первая международная конференция 2008 г. (стр. 1–5). IEEE.

[17] Скоординированное разрешение и обнаружение конфликтов с помощью самолетов, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/. Архивировано 5 марта 2016 г. в Wayback Machine.

[18] «Ателье Б» . www.atelierb.eu .

[19] CT Chou, PK Mannava, S. Park, « Простой метод параметризованной проверки протоколов когерентности кэша », Формальные методы в автоматизированном проектировании, стр. 382–398, 2004.

[20] Формальная проверка в механизме выполнения процессора Intel Core i7, http://cps-vo.org/node/1371. Архивировано 3 мая 2015 г. на Wayback Machine , по состоянию на 13 сентября 2013 г.

[21] Дж. Гранди, «Проверенная оптимизация для архитектуры Intel IA-64», В «Доказательстве теорем в логике высшего порядка», Springer Berlin Heidelberg, 2004, стр. 215–232.

[22] Э. Селигман, И. Яром, « Наиболее известные методы использования Cadence Conformal LEC », в Intel.

[23] К. Эйснер, А. Нахир, К. Йорав, « Функциональная проверка конструкций с силовым затвором с помощью композиционных рассуждений». ^{[ постоянная мертвая ссылка ]}", Компьютерная проверка, Springer Berlin Heidelberg, стр. 433–445.

[24] ПК Атти, Х. Чоклер, « Автоматическая проверка отказоустойчивых эмуляций регистров », Электронные заметки в теоретической информатике, том. 149, нет. 1, стр. 49–60.

[25] К.Д. Шуберт, В. Рознер, Дж. М. Ладден, Дж. Джексон, Дж. Бучерт, В. Парути, Б. Брок, « Функциональная проверка микропроцессора IBM POWER7 и многопроцессорных систем POWER7 », IBM Journal of Research and Development, vol. 55, № 3.

[26] X2R-2, поставка D5.1 .

[27] Дэниел Джексон и Жаннетт Винг , «Облегченные формальные методы» , IEEE Computer , апрель 1996 г.

[28] Вину Джордж и Рэйфорд Вон, «Применение облегченных формальных методов в разработке требований». Архивировано 1 марта 2006 г. в Wayback Machine , Crosstalk: Журнал оборонной разработки программного обеспечения , январь 2003 г.

[29] Дэниел Джексон, «Сплав: облегченная нотация моделирования объектов» , Транзакции ACM по разработке программного обеспечения и методологии (TOSEM) , Том 11, Выпуск 2 (апрель 2002 г.), стр. 256-290

[30] Ричард Денни, Успех в сценариях использования: разумная работа для обеспечения качества , Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6 .

[31] Стен Агерхольм и Питер Г. Ларсен, «Облегченный подход к формальным методам». Архивировано 9 марта 2006 г. в Wayback Machine , В материалах международного семинара по текущим тенденциям в прикладных формальных методах , Боппард, Германия, Springer-Verlag, октябрь 1998 г.

[32] «ЭСБМК» . esbmc.org .

[33] Барточчи, Эцио; Бейер, Дирк; Блэк, Пол Э.; Федюкович, Григорий; Гаравель, Юбер; Хартманс, Арнд; Хейсман, Марике; Кордон, Фабрис; Нагеле, Джулиан; Сигиряну, Михаэла; Штеффен, Бернхард; Суда, Мартин; Сатклифф, Джефф; Вебер, Тьярк; Ямада, Акихиса (2019). «TOOLympics 2019: Обзор соревнований по формальным методам». В Бейере, Дирк; Хейсман, Марике; Кордон, Фабрис; Штеффен, Бернхард (ред.). Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. Чам: Международное издательство Springer. стр. 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] Корнехо, Сезар (27 января 2021 г.). «Арифметическая поддержка сплавов на основе SAT» . Материалы 35-й Международной конференции IEEE/ACM по автоматизированной разработке программного обеспечения . АСЭ '20. Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. стр. 1161–1163. дои : 10.1145/3324884.3415285 . ISBN 978-1-4503-6768-4 .

[36] Барретт, Кларк; Детерс, Морган; де Моура, Леонардо; Оливерас, Альберт; Стамп, Аарон (01 марта 2013 г.). «6 лет СМТ-КОМП» . Журнал автоматизированного рассуждения . 50 (3): 243–277. дои : 10.1007/s10817-012-9246-5 . ISSN 1573-0670 .

[37] Федюкович, Григорий; Рюммер, Филипп (13 сентября 2021 г.). «Отчет о конкурсе: CHC-COMP-21» . Электронные труды по теоретической информатике . 344 : 91–108. arXiv : 2008.02939 . дои : 10.4204/EPTCS.344.7 . ISSN 2075-2180 .

[38] Шукла, Анкит; Бьер, Армин; Пулина, Лука; Зайдль, Мартина (ноябрь 2019 г.). «Обзор применения количественных логических формул» . 31-я Международная конференция IEEE по инструментам с искусственным интеллектом (ICTAI) , 2019 г. IEEE. стр. 78–84. дои : 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. дои : 10.1007/978-3-030-99527-0_20 . ISBN 978-3-030-99527-0 .

[41] Алур, Раджив; Фисман, Дана; Сингх, Ришаб; Солар-Лезама, Армандо (28 ноября 2017 г.). «СиГуС-Комп 2017: Итоги и анализ» . Электронные труды по теоретической информатике . 260 : 97–115. arXiv : 1611.07627 . дои : 10.4204/EPTCS.260.9 . ISSN 2075-2180 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

[37]

[38]

[39]

[40]

[41]

v т и Информатика
Note: This template roughly follows the 2012 ACM Computing Classification System.
Hardware	Printed circuit board Peripheral Integrated circuit Very Large Scale Integration Systems on Chip (SoCs) Energy consumption (Green computing) Electronic design automation Hardware acceleration Processor Size / Form
Computer systems organization	Computer architecture Computational complexity Dependability Embedded system Real-time computing
Networks	Network architecture Network protocol Network components Network scheduler Network performance evaluation Network service
Software organization	Interpreter Middleware Virtual machine Operating system Software quality
Software notations and tools	Programming paradigm Programming language Compiler Domain-specific language Modeling language Software framework Integrated development environment Software configuration management Software library Software repository
Software development	Control variable Software development process Requirements analysis Software design Software construction Software deployment Software engineering Software maintenance Programming team Open-source model
Theory of computation	Model of computation Formal language Automata theory Computability theory Computational complexity theory Logic Semantics
Algorithms	Algorithm design Analysis of algorithms Algorithmic efficiency Randomized algorithm Computational geometry
Mathematics of computing	Discrete mathematics Probability Statistics Mathematical software Information theory Mathematical analysis Numerical analysis Theoretical computer science
Information systems	Database management system Information storage systems Enterprise information system Social information systems Geographic information system Decision support system Process control system Multimedia information system Data mining Digital library Computing platform Digital marketing World Wide Web Information retrieval
Security	Cryptography Formal methods Security hacker Security services Intrusion detection system Hardware security Network security Information security Application security
Human–computer interaction	Interaction design Social computing Ubiquitous computing Visualization Accessibility
Concurrency	Concurrent computing Parallel computing Distributed computing Multithreading Multiprocessing
Artificial intelligence	Natural language processing Knowledge representation and reasoning Computer vision Automated planning and scheduling Search methodology Control method Philosophy of artificial intelligence Distributed artificial intelligence
Machine learning	Supervised learning Unsupervised learning Reinforcement learning Multi-task learning Cross-validation
Graphics	Animation Rendering Photograph manipulation Graphics processing unit Mixed reality Virtual reality Image compression Solid modeling
Applied computing	Quantum Computing E-commerce Enterprise software Computational mathematics Computational physics Computational chemistry Computational biology Computational social science Computational engineering Differentiable computing Computational healthcare Digital art Electronic publishing Cyberwarfare Electronic voting Video games Word processing Operations research Educational technology Document management
Category Outline Glossaries