Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Не путать с верификационизмом .
«Проверяемость» перенаправляется сюда. Политику Википедии см. Википедия: проверяемость . Для использования в других целях, см Проверка (значения) .

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

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

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

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

Один из подходов и форм - это проверка модели , которая состоит из систематически исчерпывающего исследования математической модели (это возможно для конечных моделей , но также и для некоторых бесконечных моделей, где бесконечные множества состояний могут быть эффективно представлены в конечном итоге с помощью абстракции или использования преимуществ симметрия). Обычно это состоит из исследования всех состояний и переходов в модели с использованием умных и зависящих от предметной области методов абстракции для рассмотрения целых групп состояний за одну операцию и сокращения времени вычислений. Методы реализации включают перечисление пространства состояний , символическое перечисление пространства состояний, абстрактную интерпретацию , символьное моделирование , уточнение абстракции.[ необходимая цитата ] Свойства, которые необходимо проверить, часто описываются в темпоральной логике , такой как линейная темпоральная логика (LTL), язык спецификации свойств (PSL), утверждения SystemVerilog (SVA), [3] или логика вычислительного дерева (CTL). Большим преимуществом проверки модели является то, что она часто полностью автоматическая; его основной недостаток в том, что он не масштабируется до больших систем; символические модели обычно ограничены несколькими сотнями битов состояния, в то время как явное перечисление состояний требует, чтобы исследуемое пространство состояний было относительно небольшим.

Другой подход - дедуктивная проверка. Он состоит из генерации из системы и ее спецификаций (и, возможно, других аннотаций) набора математических доказательств , истинность которых подразумевает соответствие системы ее спецификации, и выполнения этих обязательств с использованием либо помощников по доказательству (интерактивных средств доказательства теорем) ( такие как HOL , ACL2 , Isabelle , Coq или PVS ), автоматические средства доказательства теорем , включая, в частности, выполнимость по модулю теорий(SMT) решатели. Недостаток этого подхода состоит в том, что он обычно требует от пользователя детального понимания того, почему система работает правильно, и передачи этой информации в систему проверки либо в форме последовательности теорем, которые необходимо доказать, либо в форме спецификаций ( инварианты, предварительные условия, постусловия) компонентов системы (например, функций или процедур) и, возможно, подкомпонентов (таких как циклы или структуры данных).

Программное обеспечение [ править ]

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

Другим дополнительным подходом является создание программ , при котором эффективный код создается из функциональных спецификаций посредством ряда шагов по сохранению правильности. Примером такого подхода является формализм Берда – Меертенса , и этот подход можно рассматривать как еще одну форму построения правильности .

Эти методы могут быть надежными , что означает, что проверенные свойства могут быть логически выведены из семантики, или ненадежными , что означает отсутствие такой гарантии. Звуковая техника дает результат только после того, как она исследует все пространство возможностей. Примером ненадежного метода является метод, который ищет только подмножество возможностей, например, только целые числа до определенного числа, и дает "достаточно хороший" результат. Методы также могут быть разрешимыми , что означает, что их алгоритмические реализации гарантированно завершатся с ответом, или неразрешимыми, что означает, что они могут никогда не завершиться. Поскольку они ограничены, необоснованные методы часто более разрешимы, чем разумные.

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

Основная статья: Проверка и валидация

Верификация - это один из аспектов проверки соответствия продукта своему назначению. Валидация - дополнительный аспект. Часто весь процесс проверки называют V&V .

  • Валидация : «Пытаемся ли мы сделать то, что нужно?», Т. Е. Соответствует ли продукт реальным потребностям пользователя?
  • Проверка : «Сделали ли мы то, что пытались сделать?», Т. Е. Соответствует ли продукт спецификациям?

Процесс проверки состоит из статических / структурных и динамических / поведенческих аспектов. Например, для программного продукта можно проверить исходный код (статический) и запустить его с конкретными тестовыми примерами (динамический). Валидация обычно может проводиться только динамически, т. Е. Продукт тестируется путем его типичного и нетипичного использования («Удовлетворительно ли он соответствует всем вариантам использования ?»).

Автоматическое восстановление программы [ править ]

Основная статья: Автоматическое исправление ошибок

Восстановление программы выполняется по отношению к оракулу , включая желаемую функциональность программы, которая используется для проверки сгенерированного исправления. Простым примером является набор тестов - пары ввода / вывода определяют функциональность программы. Различные методы используются, прежде всего с помощью выполнимости по модулю теории (SMT) решателей, [4] и генетическое программирование , [5] с использованием эволюционного вычисления для генерации и оценки возможных кандидатов для исправления. Первый метод является детерминированным, а второй - рандомизированным.

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

Промышленное использование [ править ]

Рост сложности проектов увеличивает важность формальных методов проверки в индустрии оборудования . [6] [7] В настоящее время формальная верификация используется большинством или всеми ведущими производителями оборудования [8], но ее использование в индустрии программного обеспечения все еще не используется. [ необходима цитата ] Это может быть связано с большей потребностью в индустрии оборудования, где ошибки имеют большее коммерческое значение. [ необходима цитата ]Из-за потенциально тонких взаимодействий между компонентами становится все труднее реализовать реалистичный набор возможностей с помощью моделирования. Важные аспекты проектирования оборудования поддаются автоматизированным методам проверки, что упрощает внедрение формальной проверки и делает ее более продуктивной. [9]

По состоянию на 2011 год было официально подтверждено несколько операционных систем: микроядро NICTA Secure Embedded L4 , коммерчески продаваемое OK Labs как seL4 ; [10] OSEK / VDX операционная система реального времени ORIENTAIS Восточно-Китайского педагогического университета ; [ необходима цитата ] Операционная система Integrity Green Hills Software ; [ Править ] и SYSGO «s PikeOS . [11] [12]

В 2016 году профессора Йельского и Колумбийского университета Чжун Шао и Ронгхуэй Гу разработали формальный протокол проверки для блокчейна под названием CertiKOS. [13] Программа является первым примером формальной верификации в мире блокчейнов и примером формальной верификации, явно используемой в качестве программы безопасности. [14]

С 2017 года формальная проверка применялась к проектированию больших компьютерных сетей [15] с помощью математической модели сети [16] и в рамках новой категории сетевых технологий, сетей на основе намерений. [17] Поставщики сетевого программного обеспечения, предлагающие формальные решения для проверки, включают Cisco [18] Forward Networks [19] [20] и Veriflow Systems. [21]

Компилятор CompCert С является формально проверить компилятор реализует большинство ISO C.

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

  • Автоматическое доказательство теорем
  • Проверка модели
  • Список инструментов проверки модели
  • Формальная проверка эквивалентности
  • Проверка пруфа
  • Язык спецификации свойств
  • Избранная библиография для формальной проверки
  • Статический анализ кода
  • Временная логика в проверке с конечным числом состояний
  • Пост-силиконовая проверка
  • Интеллектуальная проверка
  • Проверка во время выполнения

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

  1. ^ Sanghavi, Alok (21 мая 2010). «Что такое формальная проверка?». EE Times Asia .
  2. ^ Введение в формальную проверку , Калифорнийский университет Беркли, последнее обращение 6 ноября 2013 г.
  3. ^ Коэн, Бен; Венкатараманан, Шринивасан; Кумари, Аджита; Пайпер, Лиза (2015). Справочник по SystemVerilog Assertions (4-е изд.). Независимая издательская платформа CreateSpace. ISBN 978-1518681448.
  4. ^ Фавио ДеМарко; Цзифэн Сюань; Даниэль Ле Берр; Мартин Монперрус (2014). Автоматическое исправление ошибки при возникновении условий и пропущенных предварительных условий с помощью SMT . Труды 6-го Международного семинара по ограничениям в тестировании, проверке и анализе программного обеспечения (CSTVA 2014) . С. 30–39. arXiv : 1404.3186 . DOI : 10.1145 / 2593735.2593740 . ISBN 9781450328470.
  5. ^ Ле Гуэ, Клэр; Нгуен, ТханьВу; Форрест, Стефани; Веймер, Уэстли (январь 2012 г.). «GenProg: общий метод автоматического восстановления программного обеспечения» . IEEE Transactions по разработке программного обеспечения . 38 (1): 54–72. DOI : 10.1109 / TSE.2011.104 .
  6. ^ Харрисон, Дж. (2003). «Формальная проверка в Intel». 18-й ежегодный симпозиум IEEE по логике в компьютерных науках, 2003. Труды . С. 45–54. DOI : 10,1109 / LICS.2003.1210044 . ISBN 978-0-7695-1884-8.
  7. ^ Формальная проверка конструкции оборудования в реальном времени . Portal.acm.org (27 июня 1983 г.). Проверено 30 апреля, 2011.
  8. ^ «Формальная проверка: важный инструмент для современной конструкции СБИС Эрика Селигмана, Тома Шуберта и М.В. Ачута Киранкумар» . 2015 г.
  9. ^ «Формальная проверка в промышленности» (PDF) . Проверено 20 сентября 2012 года .
  10. ^ "Абстрактная формальная спецификация API seL4 / ARMv6" (PDF) . Архивировано из оригинального (PDF) 21 мая 2015 года . Проверено 19 мая 2015 года .
  11. ^ Кристоф Бауманн, Бернхард Бекерт, Хольгер Бласум и Торстен Бормер Составные части правильности операционной системы? Уроки, извлеченные при формальной проверке PikeOS
  12. ^ "Все правильно" Джек Гэнссл
  13. ^ Харрис, Робин. «Невзламываемая ОС? CertiKOS позволяет создавать защищенные системные ядра» . ZDNet . Проверено 10 июня 2019 года .
  14. ^ «CertiKOS: Йельский университет разрабатывает первую в мире операционную систему, устойчивую к хакерам» . International Business Times UK . 15 ноября 2016 . Проверено 10 июня 2019 года .
  15. ^ Хеллер, Брэндон. «В поисках истины в сети: от тестирования до проверки» . Форвардные сети . Проверено 12 февраля 2018 года .
  16. ^ Скрокстон, Алекс. «Для Cisco создание сетей на основе намерений предвещает будущие потребности в технологиях» . Computer Weekly . Проверено 12 февраля 2018 года .
  17. ^ Лернер, Эндрю. «Сеть на основе намерений» . Gartner . Проверено 12 февраля 2018 года .
  18. ^ Керравала, Зевс. «Cisco привносит сети на основе намерений в центры обработки данных» . NetworkWorld . Проверено 12 февраля 2018 года .
  19. ^ «Прямые сети: ускорение и снижение рисков сетевых операций» . Insights Success . Проверено 12 февраля 2018 года .
  20. ^ "Основываясь на намерениях = сети на основе" (PDF) . NetworkWorld . Проверено 12 февраля 2018 года .
  21. ^ "Veriflow Systems" . Блумберг . Проверено 12 февраля 2018 года .