Всесторонний статический анализ с использованием продуктов Polyspace
25 февраля 2015
В статье рассматривается проблема по верификации встраиваемого программного обеспечения. Ручные или не всесторонние методы выявления дефектов и ошибок при выполнении в программном обеспечении трудозатратны и часто не реализуемы на практике для больших, сложных приложений. Динамическое же тестирование (метод «белого ящика») требует от инженеров написания и выполнения огромного числа тестов. На примерах инструментов статического анализа Polyspace описывается иной подход. Polyspace Bug Finder™ идентифицирует ошибки при выполнении, проблемы с потоками данных и другие дефекты во встраиваемом программном обеспечении, написанном на C и C++. Polyspace Code Prover™ обеспечивает гораздо более глубокий анализ, что позволяет доказывать отсутствие критических ошибок при выполнении в исходном C и C++ коде — таких, как переполнение, деление на ноль, доступ за пределы массива и других. Используются формальные методы — такие, как абстрактная интерпретация, для доказательства корректности кода.
Верификация встраиваемого программного обеспечения является сложной задачей, бросающей дополнительные вызовы, учитывая сроки и возрастающую сложность встраиваемых систем. Большинство команд, разрабатывающих программное обеспечение, полагаются на ручные или не всесторонние методы выявления дефектов и ошибок при выполнении в программном обеспечении. Рассмотрение кода трудозатратно и часто не реализуется на практике для больших, сложных приложений. Динамическое тестирование (метод «белого ящика») требует от инженеров написания и выполнения огромного числа тестов. Когда тест не выполняется, требуется дополнительное время для поиска причины ошибки путем недетерминированного процесса отладки. Тестирование не является всесторонним и нельзя полагаться только на результаты тестирования при создании надежного программного обеспечения.
Инструменты статического анализа Polyspace предлагают иной подход. Осуществляется поиск дефектов во встраиваемом программном обеспечении и используются методы, основанные на доказательстве, такие, как абстрактная интерпретация, для доказательства того, что программное обеспечение является надежным. Polyspace Bug Finder™ идентифицирует ошибки при выполнении, проблемы с потоками данных и другие дефекты во встраиваемом программном обеспечении, написанном на C и C++. Используя статический анализ, Polyspace Bug Finder анализирует потоки данных, потоки управления и межпроцедурное взаимодействие в программе. Это позволяет выявлять и устранять программные дефекты на ранних стадиях процесса разработки.
Polyspace Code Prover™ обеспечивает гораздо более глубокий анализ, что позволяет доказывать отсутствие критических ошибок при выполнении в исходном C и C++ коде — таких, как переполнение, деление на ноль, доступ за пределы массива и других. Используются формальные методы — такие, как абстрактная интерпретация, для доказательства корректности кода. По результатам верификации Polyspace Code Prover отмечает каждую операцию цветом, указывающим, содержит ли эта операция ошибки при выполнении, является недостижимой или недоказанной.
Скачать статью полностью можно по ссылке ниже.
