Polyspace Code Prover помечает результаты анализа цветом
Polyspace Code Prover помечает результаты анализа цветом

Polyspace Code Prover - это инструмент для надежного статического анализа, который доказывает отсутствие переполнения, деления на ноль, доступа за пределы границ массива и других ошибок времени выполнения в исходном коде C и C++. Данный анализ выполняется без выполнения программы, инструментации кода или тестовых векторов. Polyspace Code Prover использует семантический анализ и абстрактную интерпретацию, основанную на формальных методах, для проверки межпроцедурного взаимодействия, потоков данных и управления программного обеспечения. Инструмент используется для верификации рукописного кода, сгенерированного кода или их комбинации. Каждый оператор кода помечается цветом который указывает, доказано ли отсутствие или наличие ошибок времени исполнения, или же данный оператор недостижим или отсутствие ошибок времени исполнения не доказано.

Polyspace Code Prover отображает информацию о диапазоне для переменных и возвращаемых значений функций и может доказать, какие переменные превышают заданные пределы диапазона. Результаты верификации кода используются для отслеживания показателей качества ПО и проверки соответствия данным целям качества. Polyspace Code Prover можно использовать с Eclipse IDE для проверки кода на рабочем столе.

Для доказательства соответствия отраслевым стандартам применяются IEC Certification Kit (for ISO 26262 and IEC 61508) и DO Certification Kit (for DO-178).

Polyspace Code Prover помечает результаты анализа цветом
Polyspace Code Prover помечает результаты анализа цветом

Верификация кода с использованием формальной математики

Иерархия
Иерархия
Иерархия Иерархия

Polyspace Code Prover определяет операции кода C/C++, которые никогда не будут вызывать ошибки времени исполнения, независимо от условий выполнения. Все пути исполнения кода по всем возможным входам анализируются без запуска кода. Таким образом удовлетворяются требования по сертификации для проектов, основанных на отраслевых стандартах.

Улучшение кода и анализа

Всплывающая подсказка показывает диапазоны значений переменных и операторов
Всплывающая подсказка показывает диапазоны значений переменных и операторов

Polyspace Code Prover сокращает время, затрачиваемое на проверку кода, отладку и тестирование на робастность. Проверяются потоки управления и потоки данных программного обеспечения и вычисляются диапазоны переменных и операторов. Идентифицируются все разделы кода, которые не могут быть достигнуты в каком-либо пути исполнения и ошибки в логике и структуре программы. Polyspace Code Prover верифицирует сгенерированный код и создает трассируемость до блока исходной модели Simulink.

Всплывающая подсказка показывает диапазоны значений переменных и операторов Всплывающая подсказка показывает диапазоны значений переменных и операторов

Автоматизация верификацию кода с помощью сервера Polyspace Code Prover

Отправка оповещений о результатах статического анализа
Отправка оповещений о результатах статического анализа
Отправка оповещений о результатах статического анализа Отправка оповещений о результатах статического анализа

Polyspace Code Prover Server служит для автоматизации верификации кода, обеспечивая запуск движка Polyspace Code Prover в серверной среде с такими средами непрерывной интеграции, как Jenkins и Bamboo. Дефекты автоматически назначаются владельцам компонентов, отправляются уведомления по электронной почте. Результаты верификации могут быть загружены в Polyspace Code Prover Access, для последующей сортировки и исправления дефектов.

Совместная работа с Polyspace Code Prover Access

Суммарная информация о проекте в Polyspace Code Prover Access
Суммарная информация о проекте в Polyspace Code Prover Access

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

Суммарная информация о проекте в Polyspace Code Prover Access
Суммарная информация о проекте в Polyspace Code Prover Access