Продукты Polyspace® проверяют C, C++ и код Ады путем обнаружения ошибок времени выполнения, прежде чем код будет скомпилирован и выполнен.
Чтобы проверить исходный код, вы настраиваете параметры верификации в проекте, запускаете верификацию и рассматриваете результаты. Графический интерфейс пользователя помогает вам эффективно рассмотреть результаты верификации. Программное обеспечение присваивает цвет операциям в исходном коде можно следующим образом:
Зеленый – Указывает, что операция, как доказывают, не имеет определенные виды ошибки.
Красный – Указывает, что операция, как доказывают, имеет по крайней мере одну ошибку.
Серый – Указывает на недостижимый код.
Оранжевый – Указывает, что операция может иметь ошибку вдоль некоторых путей к выполнению.
Цветовое кодирование помогает вам быстро идентифицировать ошибки и найти точное местоположение ошибки в исходном коде. После того, как вы зафиксируете ошибки, можно легко запустить верификацию снова.
Верификация Polyspace может помочь вам к:
Программное обеспечение Polyspace улучшает надежность ваших приложений C/C++ путем доказательства корректности кода и идентификации ошибок времени выполнения. Используя усовершенствованные методы верификации, программное обеспечение Polyspace выполняет исчерпывающую верификацию вашего исходного кода.
Поскольку программное обеспечение Polyspace проверяет все подписания вашего кода, оно может идентифицировать код что:
Никогда не имеет ошибку
Всегда имеет ошибку
Недостижимо
Может иметь ошибку
С этой информацией вы знаете, сколько из вашего кода не содержит ошибки времени выполнения, и можно улучшить надежность кода путем фиксации ошибок.
Можно также улучшить качество кода при помощи программного обеспечения верификации Polyspace, чтобы проверять, что код выполняет установленные стандарты кодирования, такие как MISRA C®, MISRA® C ++ или JSF® C ++ standards.[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.