Действительно ли статический анализ является формальной проверкой?

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

Как это может быть формальная проверка, если нет формального описания модели?

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

Обратите внимание, что моделирование / формальная спецификация НЕ ЯВЛЯЕТСЯ частью статического анализа.
Однако в совокупности оба этих инструмента полезны при формальной проверке.

Например, если система моделируется как конечный автомат (FSM) с

• заранее определенное количество состояний
  определяется комбинацией определенных значений определенных данных элемента.
• предопределенный набор переходов между различными состояниями
  определяется списком функций-членов.

Тогда результаты статического анализа помогут в формальной проверке того факта, что управление НИКОГДА не течет по пути, который НЕ присутствует в приведенной выше модели конечного автомата.

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

_{ПРИМЕЧАНИЕ 1. Желтая область выше - это статические анализаторы, используемые для обеспечения соблюдения таких вещей, как рекомендации по кодированию и соглашения об именах, то есть аспекты кода, которые не могут повлиять на поведение программы.}

_{ПРИМЕЧАНИЕ 2. Красная область выше будет формальной проверкой, требующей дополнительных шагов, таких как 100% динамическое покрытие кода, удаление неиспользуемого и мертвого кода. Их нельзя обнаружить / применить с помощью статического анализатора.}

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

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

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

например. Стандарт MISRA-C для автомобильного программного обеспечения определяет подмножество C для использования в автомобильных системах.

MISRA-C: 2012 содержит

• 143 правила - каждое из которых проверяется с помощью статического программного анализа.

• 16 «директив» более открыты для интерпретации или связаны с процессом.

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

Существует множество различных типов возможных жалоб на статический анализ. Одна из возможных жалоб может заключаться в следующем:

 Your source code does not provably satisfy a formal specification

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

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

«Сверхмощные» статические анализаторы, такие как Coverity и т. Д., Имеют довольно хорошие программные модели, но они не говорят вам, что ваш код соответствует спецификации (они даже не смотрят, есть ли она у вас). В лучшем случае они только говорят вам, что ваш код делает что-то неопределенное в соответствии с языком («разыменование нулевого указателя»), и даже эта жалоба не всегда верна.

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

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

как это может быть формальная проверка, если нет формального описания модели?

Для инструментов статического анализа модель является неявной (или в некоторых инструментах частично неявной). Например, «правильно сформированная программа на C ++ не будет пропускать память и не будет обращаться к памяти, которая не была инициализирована». Такого рода правила могут быть выведены из спецификации языка или из стандартов кодирования конкретного проекта.