Polyspace® продукты проверяют код C, C++ и код Ada путем обнаружения ошибок времени выполнения перед компиляцией и выполнением кода.
Чтобы проверить исходный код, вы настраиваете параметры верификации в проекте, запускаете верификацию и просматриваете результаты. Графический пользовательский интерфейс помогает вам эффективно просматривать результаты верификации. Программа присваивает цвет операциям в исходном коде следующим образом:
Зеленый - указывает, что операция не имеет определенных видов ошибок.
Красный - указывает, что операция имеет хотя бы одну ошибку.
Серый - указывает на недостижимый код.
Orange - указывает, что операция может иметь ошибку на некоторых путях выполнения.
Цветовое кодирование помогает быстро идентифицировать ошибки и найти точное местоположение ошибки в исходном коде. После того, как вы исправите ошибки, можно легко запустить верификацию снова.
Polyspace верификации может помочь вам в:
Программное обеспечение Polyspace повышает надежность приложений C/C + +, доказывая корректность кода и идентифицируя ошибки времени выполнения. Используя расширенные методы верификации, программное обеспечение Polyspace выполняет исчерпывающую верификацию вашего исходного кода.
Поскольку программное обеспечение Polyspace проверяет все исполнения вашего кода, оно может идентифицировать код, который:
Никогда не имеет ошибки
Всегда имеет ошибку
Недоступен
Возможно, произошла ошибка
С помощью этой информации вы знаете, какая часть вашего кода не содержит ошибок времени выполнения, и можно улучшить надежность вашего кода, исправив ошибки.
Вы также можете улучшить качество своего кода, используя программное обеспечение верификации Polyspace, чтобы проверить, что ваш код соответствует установленным стандартам кодирования, таким как MISRA C®, MISRA® C++ или JSF® Стандарты C++.[1]
Программное обеспечение Polyspace сокращает время разработки, автоматизируя процесс верификации и помогая вам эффективно просматривать результаты верификации. Использовать его можно в любой момент процесса разработки. Однако использование его во время ранних фаз кодирования позволяет вам находить ошибки, когда исправить их менее дорого.
Вы используете программное обеспечение Polyspace, чтобы проверить исходный код перед компиляцией времени. Чтобы проверить исходный код, вы настраиваете параметры верификации в проекте, запускаете верификацию и просматриваете результаты. Этот процесс занимает значительно меньше времени, чем с помощью ручных методов или с помощью инструментов, которые требуют, чтобы вы изменяли код или запускали тесты.
Цветовое кодирование результатов помогает быстро идентифицировать ошибки. Вы будете тратить меньше времени на отладку, потому что вы можете увидеть точное местоположение ошибки в исходном коде. После того, как вы исправите ошибки, можно легко запустить верификацию снова.
Программное обеспечение верификации Polyspace помогает вам эффективно использовать свое время. Поскольку вы знаете части вашего кода, которые не имеют ошибок, можно сосредоточиться на коде с проверенным (красный код) или потенциальными ошибками (оранжевый код).
Просмотр кода, который может иметь ошибки (оранжевый код), может занять много времени, но программное обеспечение Polyspace помогает вам в процессе проверки. Можно использовать фильтры, чтобы фокусироваться на определенных типах ошибок или можно позволить программному обеспечению идентифицировать код, который вы должны просмотреть.
Программное обеспечение Polyspace облегчает совместное использование параметров и результатов верификации, позволяя группе разработчиков работать вместе для повышения надежности продукта. После настройки параметров верификации разработчики могут повторно использовать их для других файлов в том же приложении.
Программное обеспечение верификации Polyspace поддерживает верификацию кода в течение всего процесса разработки:
Отдельный разработчик может найти и исправить ошибки времени выполнения во время начальной фазы кодирования.
Инженеры по обеспечению качества могут проверить общую надежность приложения.
Менеджеры могут контролировать надежность приложений путем создания отчетов по результатам верификации.
Программное обеспечение Polyspace использует статическую верификацию, чтобы доказать отсутствие ошибок времени выполнения. Статическая верификация выводит динамические свойства программы, не выполняя её на самом деле. Это значительно отличается от других методов, таких как отладка во время выполнения, тем, что предоставляемая ею верификация не основана на заданном тесте или наборе тестов. Динамические свойства, полученные в верификации Polyspace, верны для всех выполнений программного обеспечения.
Статическая верификация является широким термином и применима к любому инструменту, который выводит динамические свойства программы без выполнения программы. Однако большинство инструментов статической верификации только проверяют сложность программного обеспечения в поиске конструкций, которые могут быть потенциально ошибочными. Polyspace верификации обеспечивает глубокие верификации, идентифицирующие почти все ошибки времени выполнения и возможные конфликты доступа с глобальными разделяемыми данными.
Проверка Polyspace работает путем аппроксимации ПО под проверку, с помощью репрезентативных приближений операций ПО и данных.
Например, рассмотрим следующий код:
for (i=0 ; i<1000 ; ++i)
{ tab[i] = foo(i);
}Чтобы проверить, что переменная i никогда не переполняет область значений tabтрадиционным подходом было бы перечисление каждого возможного значения i. Потребуется одна тысяча проверок.
Используя статический подход верификации, переменная i моделируется его изменением в области. Для образца - модель i заключается в том, что он принадлежит статическому интервалу [0.. 999]. (В зависимости от сложности данных для этой цели также используются выпуклые многогранники, целочисленные решетки и более проработанные модели ).
По определению приближение приводит к потере информации. Например, информация, которая i увеличивается на единицу каждый цикл в цикле теряется. Однако важным фактом является то, что эта информация не требуется для того, чтобы гарантировать отсутствие ошибки области значений; необходимо только доказать, что изменение области i меньше диапазона tab. Требуется только одна проверка, чтобы установить, что - и, следовательно, повышение эффективности по сравнению с традиционными подходами.
Статическая верификация кода имеет точное решение. Однако это точное решение не является практичным, поскольку это потребует перечисления всех возможных тестов. В результате для полезного инструмента требуется приближение.
С точки зрения исчерпанности ничего не потеряно. Причина в том, что верификация Polyspace работает путем выполнения верхних приближений. Другими словами, вычисленная область изменений программной переменной является верхним набором ее фактической области изменения. В результате Polyspace проверяет элементы ошибки времени выполнения, которые требуют проверки.
[1] MISRA и MISRA C являются зарегистрированными товарными знаками MISRA Ltd., принадлежащими консорциуму MISRA.