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

Что входит в курс:

  • Создание проекта верификации;
  • Исследование и понимание результатов верификации;
  • Эмуляция исполнения кода на целевой платформе;
  • Работа с отсутствующими функциями и данными;
  • Работа с неподтвержденным кодом (отмечен оранжевым в инструментах Polyspace);
  • Ррименение правил написания кода MISRA;
  • Создание отчетов.

Предварительная подготовка:

Серьезные знания C, C++.

Продолжительность курса - 2 дня.

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

Программа

  • Введение в инструменты верификации кода Polyspace.
  • Polyspace Bug Finder.
  • Анализ результатов верификации Polyspace Code Prover.
  • Проверки исходного кода.
  • Управление верификацией и ее результатами.
  • Улучшение точности верификации.
  • Анализ интеграции ПО.
  • Метрики и отчеты о качестве ПО.
  • Анализ приложений.

Введение в инструменты верификации кода Polyspace

Цель: ознакомление с инструментами Polyspace и работа с начальным примером.

  • Процесс разработки ПО с Polyspace;
  • Простейший пример верификации;
  • Анализ дефектов и ошибок времени исполнения.

Polyspace Bug Finder

Цель: верификация кода, не соответствующего требованиям ANSI C, с учетом среды исполнения и устранение дефектов и нарушений стандарта кодирования с помощью Polyspace Bug Finder.

  • Основные артефакты среды исполнения;
  • Работа с кодом, написанным для определенного процессора;
  • Определение контекста исполнения;
  • Задание параметров аппаратного обеспечения;
  • Анализ и управление обнаруженными дефектами ПО;
  • Обнаружение нарушений стандарта кодирования.

Анализ результатов верификации Polyspace Code Prover

Цель: эффективный анализ результатов работы Polyspace Code Prover.

  • Обзор абстрактной интерпретации;
  • Анализ дерева вызовов;
  • Навигация по исходному коду;
  • Выполняемые ветви;
  • Диапазон значений переменной;
  • Глобальные переменные.

Проверки исходного кода

Цель: обнаружение ошибок времени исполнения с помощью диагностик Polyspace Code Prover

  • Обзор проверок С кода;
  • Описание проверок;
  • Настройка верификации.

Управление верификацией и ее результатами

Цель: работа с результатами верификации, содержащими большое количество неподтвержденных маркеров («оранжевые»).

  • Определение затрат на верификацию;
  • Быстрый обзор;
  • Избирательный обзор;
  • Определение точности верификации;
  • Определение приоритетов оранжевых маркеров;
  • Обзор оранжевых маркеров.

Улучшение точности верификации

Цель: изучение работы Polyspace с отсутствующим кодом во время верификации, способов влияния на это поведение для получения более точных результатов.

  • Проверка робастности ПО и контекстная верификация;
  • Создание «заглушек» для функций;
  • Определение диапазона данных.

Анализ интеграции ПО

Цель: ознакомиться с управлением верификации сложного кода и интерпретацией результатов интеграции ПО с помощью анализа на робастность

  • Управление модулями кода;
  • Анализ дефектов интеграции с Polyspace Bug Finder и Polyspace Code Prover;
  • Импорт комментариев.

Метрики и отчеты о качестве ПО

Цель: применение веб-сервера Polyspace Metrics для хранения результатов верификации, и генерация стандартных отчетов по результатам верификации.

  • Предоставление общего доступа к результатам верификации;
  • Использование Polyspace Metrics;
  • Проверка требований к качеству ПО;
  • Создание документации.

Анализ приложений

Цель: обзор процедур и настроек, позволяющих упростить верификацию всего приложения.

  • Настройка верификации приложения;
  • Улучшение результатов верификации;
  • Обнаружение дефектов многопоточности;
  • Сравнение проверок на робастность и контекстной верификации.

Услуги

Продукты

Выберите компанию из списка
Новый email