Продукты Polyspace для анализа и верификации кода

Polyspace® продукты используют статический анализ для проверки кода на ошибки времени выполнения, стандартные нарушения кодирования, уязвимости безопасности и другие проблемы:

  • Статический анализ, такой как Polyspace Code Prover™, может охватывать все возможные пути выполнения через программу и отслеживать поток данных по этим путям в соответствии с определенными математическими правилами. Исчерпывающий анализ управления и потока данных может дополнить динамическую проверку и выявить потенциальные ошибки времени выполнения, которые в противном случае не могут быть обнаружены при регулярной проверке на робастность.

  • Статический анализ, такой как Polyspace Bug Finder™, может сканировать программу на более очевидные ошибки времени выполнения, уязвимости безопасности, стандартные нарушения кодирования и другие проблемы, которые потенциально приводят к ошибкам времени выполнения или неожиданным результатам.

Использование продуктов Polyspace в разработке программного обеспечения

Набор продуктов Polyspace поддерживает все фазы процесса разработки ПО:

  • Перед отправкой кода:

    Разработчики могут запустить рабочий стол Polyspace или продукты, ориентированные на IDE, чтобы проверить их код во время разработки или непосредственно перед отправкой для достижения предопределенных целей качества.

    Продукты могут быть интегрированы в такие среды IDE, как Visual Studio Code, Visual Studio или Eclipse™, или запускаться со скриптами во время компиляции. Результаты анализа можно просмотреть в IDE или в графическом интерфейсе пользователя настольных продуктов.

    Polyspace предоставляет следующие продукты для использования на рабочем столе. Эти продукты предназначены для выполнения на полных проектах или небольших модулях кода (вплоть до одного исходного файла).

    • Polyspace Bug Finder , чтобы проверить код на семантические ошибки, которые компилятор не может обнаружить (такие как использование = вместо ==), проблемы параллелизма, уязвимости безопасности и другие дефекты исходного кода C и C++. Анализ также может обнаружить некоторые ошибки времени выполнения.

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

  • После подачи кода:

    Серверные продукты Polyspace могут запускаться автоматически на только что зафиксированном коде в качестве шага сборки в процессе непрерывного интегрирования (используя такие инструменты, как Jenkins). Анализ выполняется на сервере, и результаты загружаются в веб-интерфейс для совместной проверки.

    Polyspace предоставляет следующие продукты для использования серверами:

    • Polyspace Bug Finder Server™ автоматически запускать Bug Finder на сервере и загружать результаты в веб-интерфейс для просмотра, а Polyspace Bug Finder Access™ для просмотра загруженных результатов.

    • Polyspace Code Prover Server автоматически запускает Code Prover на сервере и загружает результаты в веб-интерфейс для проверки, и Polyspace Code Prover Access для просмотра загруженных результатов.

Как правило, Polyspace Bug Finder Server (или Polyspace Code Prover Server) работает на нескольких серверах сборки и проверяет новый зафиксированный код как часть сборки и проверки программного обеспечения. Каждый рецензент (разработчик, инженер по обеспечению качества или руководитель разработки) имеет лицензию Polyspace Bug Finder Access (или Polyspace Code Prover Access) для проверки загруженных результатов анализа.

В сложение, если разработчики имеют доступ к Polyspace Bug Finder Access для веб-обзора результатов после отправки, они также могут установить Polyspace, как вы Кодами в их IDE для предварительного анализа. При установке в качестве расширения IDE Polyspace as You Code выполняет file-scope Bug Finder-подобный анализ и обеспечивает почти мгновенную обратную связь разработчикам во время кодирования.

Эта схема показывает одно возможное развертывание продуктов Polyspace.

При использовании как рабочем столе, так и серверных продуктов рабочий процесс перед отправкой может плавно переходить к рабочему процессу после отправки.

Координация использования Polyspace до и после отправки

Когда вы запускаете более одного продукта Polyspace на отдельных этапах рабочего процесса разработки ПО, более поздние запуски могут быть полезны при более раннем использовании и наоборот. В частности:

  • Разработчики, использующие Polyspace в качестве You Code в своих IDE, могут легко исправить дефекты и стандартные нарушения кодирования, которые можно найти и устранить в одном файле. Более поздний анализ Polyspace Bug Finder Server после подачи кода больше не показывает эти проблемы.

  • Результаты анализа Polyspace Bug Finder Server могут действовать как базовая линия для Polyspace при запусках You Code. Разработчики, использующие последний результат Polyspace Bug Finder Server, поскольку базовый уровень для их запусков в IDE может фокусироваться только на проблемах, возникающих в результате изменений их кода.

Polyspace Products for Ada Кода

Polyspace предоставляет эти продукты для проверки кода Ada:

  • Polyspace Client™ , чтобы Ada проверяла код Ada на ошибки времени выполнения на рабочем столе.

  • Polyspace Server для Ada , чтобы проверить код Ada на ошибки времени выполнения на сервере.

Можно использовать настольный продукт для выполнения анализа на рабочем столе или комбинация настольных и серверных продуктов для выполнения анализа на сервере. Результаты анализа загружаются на рабочий стол для просмотра.

Если у вас есть лицензия Polyspace Code Prover Access и вы настроили веб-интерфейс Polyspace Code Prover Access, можно загрузить каждый отдельный результат Ada из десктопных продуктов Ada в веб-интерфейс для совместной проверки.

См. также:

Похожие темы