Введение

Доказательство или опровержение корректности определенных задуманных алгоритмов.

В контексте аппаратных и программных систем, формальная верификация – это процесс доказательства или опровержения корректности системы относительно определенной формальной спецификации или свойства с использованием формальных математических методов. Формальная верификация является ключевым стимулом для формального описания систем и лежит в основе формальных методов. Она представляет собой важную область анализа и проверки в автоматизированном проектировании электроники и является одним из подходов к верификации программного обеспечения. Использование формальной верификации позволяет достичь наивысшего уровня гарантии оценки (EAL7) в рамках общих критериев сертификации компьютерной безопасности. Формальная верификация может быть полезна для доказательства корректности систем, таких как: криптографические протоколы, комбинационные схемы, цифровые схемы с внутренней памятью и программное обеспечение, представленное в виде исходного кода на языке программирования. Яркими примерами верифицированных программных систем являются верифицированный C-компилятор CompCert и ядро операционной системы seL4 с высокой степенью надежности. Верификация этих систем осуществляется путем обеспечения наличия формального доказательства математической модели системы. Примеры математических объектов, используемых для моделирования систем: конечные автоматы, системы с помеченными переходами, клаузы Хорна, сети Петри, системы векторного сложения, автоматы с временными ограничениями, гибридные автоматы, алгебра процессов, формальная семантика языков программирования, такая как операционная семантика, денотационная семантика, аксиоматическая семантика и логика Хоара.

Подходы

Один из подходов – проверка модели, которая заключается в систематическом и исчерпывающем исследовании математической модели (это возможно для конечных моделей, но также и для некоторых бесконечных моделей, где бесконечные множества состояний могут быть эффективно представлены в конечном виде с помощью абстракции или использования симметрии). Обычно это предполагает исследование всех состояний и переходов в модели, с использованием интеллектуальных и специализированных методов абстракции для рассмотрения целых групп состояний за одну операцию и сокращения времени вычислений. Методы реализации включают перечисление пространства состояний, символическое перечисление пространства состояний, абстрактную интерпретацию, символическое моделирование, уточнение абстракции. Свойства, подлежащие проверке, часто описываются во временных логиках, таких как линейная временная логика (LTL), язык спецификации свойств (PSL), SystemVerilog Assertions (SVA) или логика вычислительного дерева (CTL). Главное преимущество проверки модели – её часто полная автоматизация; её основной недостаток – плохая масштабируемость для больших систем: символические модели обычно ограничены несколькими сотнями битов состояния, а явное перечисление состояний требует, чтобы исследуемое пространство состояний было относительно небольшим. Другой подход – дедуктивная верификация. Он заключается в генерации из системы и её спецификаций (и, возможно, других аннотаций) набора математических доказательственных обязательств, истинность которых подразумевает соответствие системы её спецификации, и выполнении этих обязательств с использованием либо помощников доказательства (интерактивных доказателей теорем) (таких как HOL, ACL2, Isabelle, Coq или PVS), либо автоматических доказателей теорем, в частности решателей задач выполнимости с учетом теорий (SMT). Недостатком этого подхода является то, что он может потребовать от пользователя детального понимания принципов работы системы и передачи этой информации в систему верификации либо в форме последовательности теорем для доказательства, либо в форме спецификаций (инвариантов, предусловий, постусловий) компонентов системы (например, функций или процедур) и, возможно, подкомпонентов (таких как циклы или структуры данных).

Программное обеспечение

Формальная проверка программного обеспечения включает в себя доказательство того, что программа соответствует формальной спецификации её поведения. Области формальной верификации включают дедуктивную верификацию (см. выше), абстрактную интерпретацию, автоматическое доказательство теорем, системы типов и облегчённые формальные методы. Многообещающим подходом к верификации на основе типов является программирование с зависимыми типами, в котором типы функций включают (по крайней мере часть) спецификаций этих функций, а проверка типов кода устанавливает его корректность относительно этих спецификаций. Полнофункциональные языки с зависимыми типами поддерживают дедуктивную верификацию как частный случай. Другим дополнительным подходом является вывод программы, при котором эффективный код генерируется из функциональных спецификаций посредством серии шагов, сохраняющих корректность. Примером такого подхода является формализм Бёрда — Мертенса, и этот подход можно рассматривать как ещё одну форму корректности посредством построения. Эти методы могут быть надёжными, то есть проверенные свойства могут быть логически выведены из семантики, или ненадежными, то есть такая гарантия отсутствует. Надёжный метод выдаёт результат только после охвата всего пространства возможностей. Примером ненадежного метода является тот, который охватывает лишь подмножество возможностей, например, только целые числа до определённого значения, и выдаёт "достаточно хороший" результат. Методы также могут быть разрешимыми, то есть их алгоритмические реализации гарантированно завершаются с ответом, или неразрешимыми, то есть они могут не завершиться никогда. Ограничивая область возможностей, можно построить ненадежные, но разрешимые методы, когда разрешимых надёжных методов не существует.

Проверка и валидация

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

Валидация отвечает на вопрос: "Правильную ли вещь мы создаём?", то есть, соответствует ли продукт фактическим потребностям пользователя? Проверка отвечает на вопрос: "Сделали ли мы то, что планировали?", то есть, соответствует ли продукт спецификациям? Процесс проверки включает в себя статические/структурные и динамические/поведенческие аспекты. Например, для программного продукта можно провести анализ исходного кода (статический) и выполнить тестирование по конкретным сценариям (динамический). Валидация обычно выполняется только динамически, то есть продукт тестируется в типичных и нетипичных сценариях использования ("Удовлетворительно ли он реализует все случаи использования?").

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

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