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 определяет операции кода 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 и показателей качества в веб-интерфейсе, а также их центральное хранилище. Инструменты навигации для исследования результатов статического анализа отображаются рядом с кодом. Информационные панели отображают информацию, которую можно использовать для отслеживания качества программного обеспечения, состояния проекта, количества дефектов и метрик кода. Веб-интерфейс также обеспечивает создание и назначение заявок в таких инструментах отслеживания ошибок, как Jira.
Доказательство отсутствия Run-Time ошибок во встраиваемом C/С++ коде (PSCC)
Верификация С/С++ кода с Polyspace
