Является ли статический анализ действительно формальной проверкой?
Я читал о формальной проверке, и суть в том, что для работы требуются формальная спецификация и модель. Однако многие источники классифицируют статический анализ как метод формальной проверки, некоторые упоминают абстрактную интерпретацию и упоминают ее использование в компиляторах. Поэтому я запутался - как это может быть формальной проверкой, если нет формального описания модели?
РЕДАКТИРОВАТЬ: Источник, который я нашел, читает:
Статический анализ: абстрактная семантика вычисляется автоматически из текста программы в соответствии с предопределенными абстракциями (которые иногда могут настраиваться пользователем автоматически / вручную)
Значит ли это, что он работает только с исходным кодом без необходимости формальной спецификации? Это то, что делают статические анализаторы.
Кроме того, возможен ли статический анализ без формальной проверки? Например, SonarQube действительно выполняет формальные методы?
3 ответа
В контексте аппаратных и программных систем формальная проверка - это акт подтверждения или опровержения правильности предполагаемых алгоритмов, лежащих в основе системы в отношении определенной формальной спецификации или свойства, с использованием формальных методов математики.
Как это может быть формальной проверкой, если нет формального описания модели?
Статический анализатор будет генерировать поток управления / данных для фрагмента кода, после чего могут быть применены формальные методы для проверки соответствия ожидаемой модели проектирования системы / устройства.
Обратите внимание, что моделирование / формальная спецификация НЕ является частью статического анализа.
Несмотря на то, что оба эти инструмента объединены вместе, они полезны для формальной проверки.
Например, если система моделируется как конечный автомат (FSM) с
- заранее определенное количество состояний
определяется комбинацией конкретных значений определенных данных члена. - предопределенный набор переходов между различными состояниями
определяется списком функций-членов.
Тогда результаты статического анализа помогут в формальной проверке того факта, что
управление НИКОГДА не течет по пути, который НЕ присутствует в вышеупомянутой модели FSM.
Кроме того, если модель может быть просто определена в терминах определения типа, потока данных, потока управления / графа вызовов, то есть метрик кода, которые может проверить статический анализатор, то самого статического анализа достаточно для формальной проверки этот код соответствует такой модели. 
NOTE1. Желтая область выше - это статические анализаторы, используемые для реализации таких вещей, как правила кодирования и соглашения об именах, то есть аспекты кода, которые не могут влиять на поведение программы.
ЗАМЕТКА 2. Красная область выше была бы формальной проверкой, которая требует дополнительных шагов, таких как 100% динамическое покрытие кода, устранение неиспользованного и мертвого кода. Они не могут быть обнаружены / применены с помощью статического анализатора.
Статический анализ очень эффективен при проверке того, что система / блок реализована с использованием подмножества языковой спецификации для достижения целей, изложенных в проекте системы / блока.
Например, если целью проекта является предотвращение превышения определенного предела памяти стека, то можно применить ограничение на глубину рекурсии (или вообще запретить вызовы рекурсивных функций). Статический анализ используется для выявления таких нарушений проектных целей.
При отсутствии каких-либо предупреждений от статического анализатора,
код системы / модуля формально проверяется на соответствие таким целям разработки соответствующей модели.
например. Стандарт MISRA-C для автомобильного программного обеспечения определяет подмножество C для использования в автомобильных системах.
MISRA-C: 2012 содержит
143 правила - каждое из которых можно проверить с помощью статического анализа программы.
16 "директив" более открыты для интерпретации или имеют отношение к процессу.
Статический анализ просто означает "прочитать исходный код и, возможно, пожаловаться". (В отличие от "динамического анализа", означающего "запустить программу и, возможно, пожаловаться на некоторое поведение при выполнении").
Существует множество различных типов жалоб на статический анализ. Одна возможная жалоба может быть,
Your source code does not provably satisfy a formal specification
Эта жалоба основывалась бы на формальной проверке, если бы у статического анализатора была формальная спецификация, которую он интерпретировал "формально", формальная интерпретация исходного кода и проверенный доказатель теоремы, который не мог найти подходящую теорему.
Все другие виды жалоб, которые вы можете получить от статического анализатора, являются в значительной степени эвристическими мнениями, то есть они основаны на неформальной интерпретации кода (или спецификации, если она действительно существует).
"Сверхмощные" статические анализаторы, такие как Coverity и т. Д., Имеют довольно хорошие программные модели, но они не говорят вам, что ваш код соответствует спецификации (они даже не проверяют, есть ли у вас такой код). В лучшем случае они только говорят вам, что ваш код делает что-то неопределенное в соответствии с языком ("разыменование нулевого указателя"), и даже эта жалоба не всегда верна.
Так называемые "контролеры стиля", такие как MISRA, также являются статическими анализаторами, но их жалобы, по сути, "Вы использовали конструкцию, которая, по мнению какого-то комитета, была дурной". Это на самом деле не ошибка, это чистое мнение.
Конечно, вы можете классифицировать статический анализ как формальную проверку.
как это может быть формальной проверкой, если нет формального описания модели?
Для инструментов статического анализа модель является неявной (или в некоторых инструментах, частично неявной). Например, "правильно сформированная программа на C++ не утечет память и не получит доступ к памяти, которая не была инициализирована". Эти виды правил могут быть получены из спецификации языка или из стандартов кодирования конкретного проекта.