Войти
В контексте аппаратного обеспечения и программных систем, формальная проверка является действием доказательство или опровержение правильности предполагаемых алгоритмов, лежащих в основе системы, в отношении определенной формальной спецификации или свойства, с использованием формальных методы из математики.
Формальная проверка может быть полезна для подтверждения правильности таких систем, как: криптографические протоколы, комбинационные схемы, цифровые схемы с внутренней памятью и программным обеспечением в виде исходного кода.
Проверка этих систем осуществляется путем предоставления формального доказательства абстрактной математической модели системы, соответствия между математической моделью и характером система иначе известна по конструкции. Примеры математических объектов, часто используемых для моделирования систем: конечные автоматы, помеченные переходные системы, сети Петри, системы сложения векторов, синхронизированные автоматы, гибридные автоматы, алгебра процессов, формальная семантика языков программирования, такая как операционная семантика, денотационная семантика, аксиоматическая семантика и логика Хоара.
Один из подходов и форм - это проверка модели, которая состоит из систематически исчерпывающего исследования математической модели (это возможно для конечных моделей, но также и для некоторых бесконечных моделей, где бесконечные наборы состояний могут быть эффективно представлены в конечном итоге с помощью абстракции или использования симметрии). Обычно это состоит из исследования всех состояний и переходов в модели с использованием умных и зависящих от предметной области методов абстракции для рассмотрения целых групп состояний за одну операцию и сокращения времени вычислений. Методы реализации включают перечисление пространства состояний, символическое перечисление пространства состояний, абстрактную интерпретацию, символьное моделирование, уточнение абстракции. Проверяемые свойства часто описываются в темпоральной логике, например, линейная темпоральная логика (LTL), Язык спецификации свойств (PSL), SystemVerilog. Утверждения (SVA) или логика вычислительного дерева (CTL). Большим преимуществом проверки модели является то, что она часто полностью автоматическая; его основной недостаток заключается в том, что он не масштабируется до больших систем; символические модели обычно ограничены несколькими сотнями битов состояния, в то время как явное перечисление состояний требует, чтобы исследуемое пространство состояний было относительно небольшим.
Другой подход - дедуктивная проверка. Он состоит из генерации на основе системы и ее спецификаций (и, возможно, других аннотаций) набора математических доказательств, истинность которых подразумевает соответствие системы ее спецификации, и выполнения этих обязательств с использованием либо помощников по доказательству (интерактивные средства доказательства теорем) (например, HOL, ACL2, Isabelle, Coq или PVS ), автоматические средства доказательства теорем, включая, в частности, выполнимость по модулю теорий (SMT) решатели. Недостаток этого подхода состоит в том, что он обычно требует от пользователя детального понимания того, почему система работает правильно, и передачи этой информации системе проверки либо в форме последовательности теорем, которые необходимо доказать, либо в форме спецификаций ( инварианты, предварительные условия, постусловия) компонентов системы (например, функций или процедур) и, возможно, подкомпонентов (таких как циклы или структуры данных).
Формальная проверка программного обеспечения включает доказательство того, что программа удовлетворяет формальной спецификации ее поведения. Подразделы формальной проверки включают дедуктивную проверку (см. Выше), абстрактную интерпретацию, автоматическое доказательство теорем, системы типов и легкие формальные методы. Перспективным подходом к верификации на основе типов является программирование с зависимой типизацией, в котором типы функций включают (по крайней мере, часть) спецификации этих функций, а проверка типов устанавливает его соответствие этим спецификациям. Полнофункциональные языки с зависимой типизацией поддерживают дедуктивную проверку как особый случай.
Другим дополнительным подходом является создание программы, в котором эффективный код создается из функциональных спецификаций с помощью серии этапов сохранения корректности. Примером такого подхода является формализм Берда – Меертенса, и этот подход можно рассматривать как другую форму.
Эти методы могут быть надежными, что означает, что проверенные свойства могут быть логически выведены из семантики, или ненадежными, что означает отсутствие такой гарантии. Звуковая техника дает результат только после того, как она исследует все пространство возможностей. Примером ненадежного метода является метод, который ищет только подмножество возможностей, например, только целые числа до определенного числа, и дает "достаточно хороший" результат. Методы также могут быть разрешимыми, что означает, что их алгоритмические реализации гарантированно завершают ответом, или неразрешимыми, что означает, что они могут никогда не завершиться. Поскольку они ограничены, необоснованные методы часто более разрешимы, чем разумные.
Верификация - это один из аспектов тестирования соответствия продукта своему назначению. Валидация - дополнительный аспект. Часто общий процесс проверки называют VV.
Процесс проверки состоит из статических / структурных и динамических / поведенческих аспектов. Например, для программного продукта можно проверить исходный код (статический) и выполнить определенные тестовые случаи (динамический). Валидация обычно может выполняться только динамически, то есть продукт тестируется путем его типичного и нетипичного использования («Удовлетворительно ли он соответствует всем сценариям использования ?»).
Восстановление программы выполняется в отношении oracle, охватывая желаемые функциональные возможности программы, которая используется для проверки сгенерированного исправления. Простым примером является набор тестов - пары ввода / вывода определяют функциональность программы. Используются различные методы, в первую очередь с использованием решателей теорий выполнимости по модулю (SMT) и генетического программирования с использованием эволюционных вычислений для генерации и оценки возможных кандидатов на исправления. Первый метод является детерминированным, а второй - рандомизированным.
Восстановление программ сочетает в себе методы формальной проверки и синтеза программ. Методы локализации неисправностей в формальной верификации используются для вычисления точек программы, которые могут быть возможными местоположениями ошибок, на которые могут нацеливаться модули синтеза. Системы исправления часто фокусируются на небольшом заранее определенном классе ошибок, чтобы уменьшить пространство для поиска. Промышленное использование ограничено из-за вычислительной стоимости существующих методов.
Рост сложности проектов увеличивает важность формальных методов проверки в. В настоящее время формальная проверка используется большинством или всеми ведущими производителями оборудования, но ее использование в индустрии программного обеспечения все еще не используется. Это может быть связано с большей потребностью в индустрии оборудования, где ошибки имеют большее коммерческое значение. Из-за потенциально тонких взаимодействий между компонентами становится все труднее реализовать реалистичный набор возможностей с помощью моделирования. Важные аспекты проектирования оборудования поддаются автоматизированным методам проверки, что упрощает внедрение формальной проверки и делает ее более продуктивной.
По состоянию на 2011 год, несколько операционных систем были официально проверены: Secure Embedded L4 от NICTA, микроядро, продается OK Labs как seL4 ; Операционная система реального времени ORIENTAIS на базе OSEK / VDX от Восточно-Китайского педагогического университета ; Операционная система Integrity от Green Hills Software; и SYSGO PikeOS.
. По состоянию на 2016 год профессора Йельского университета и Колумбии Чжун Шао и Ронгхуэй Гу разработали формальный протокол проверки для блокчейна под названием CertiKOS. Программа является первым примером формальной проверки в мире блокчейнов и примером формальной проверки, явно используемой в качестве программы безопасности.
С 2017 года формальная проверка применялась к проектированию больших компьютерных сетей. с помощью математической модели сети и в рамках новой категории сетевых технологий - сетей на основе намерений. Поставщики сетевого программного обеспечения, которые предлагают формальные решения для проверки, включают Cisco Forward Networks и Veriflow Systems.
Компилятор CompCert C - это официально проверенный компилятор C, реализующий большую часть ISO C..
 | Найдите проверяемость в Wiktionary, бесплатном словаре. |
