• Новостная рассылка

    Подпишитесь и получайте самые свежие новости.
    Подписаться на новостную рассылку
  • Polyspace Code Prover для верификации C/С++ кода

    Код тренинга: PSCC

    Практикум предназначен для инженеров, ответственных за разработку программного обеспечения или моделей, применяемых для разработки встраиваемых систем. На тренинге рассматриваются следующие темы:

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

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

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

    Инструменты

    Продолжительность 2 дня.


    Программа курса:

    Модуль 1. Введение в инструменты верификации кода Polyspace
    Модуль 2. Среда компиляции для целевой платформы
    Модуль 3. Анализ результатов Polyspace
    Модуль 4. «Стабы» и определение диапазона данных
    Модуль 5. Маркеры верификации кода
    Модуль 6. Работа с оранжевыми маркерами
    Модуль 7. Проверка на соответствие MISRA-C
    Модуль 8. Метрика и отчеты для представления в сети
    Модуль 9. Контекстная верификация 


    Заявка на тренинг


    Подробнее

    Программа обучения

    Модуль 1. Введение в инструменты верификации кода Polyspace

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

    • Обзор программного обеспечения Polyspace
    • Пример верификации начального уровня
    • Выполнение удаленной верификации с использованием Polyspace Server

    Модуль 2. Среда компиляции для целевой платформы

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

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

    Модуль 3. Анализ результатов Polyspace

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

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

    Модуль 4. «Стабы» и определение диапазона данных

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

    • Верификация надежности и контекстная верификация
    • Создание «стабов»
    • Определение диапазона данных

    Модуль 5. Маркеры верификации кода

    Цель: обнаружение ошибок времени исполнения (run-time errors) с использованием инструментов Polyspace

    • Обзор маркеров исходного кода C
    • Нахождение маркеров в исходном коде
    • Описание маркеров
    • Полезные опции верификации

    Модуль 6. Работа с оранжевыми маркерами

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

    • Определение затрат на верификацию
    • Быстрый обзор (пример с ПИ-регулятором)
    • Избирательный обзор (пример с ПИ-регулятором)
    • Определение точности верификации
    • Определение приоритетов оранжевых маркеров
    • Обзор оранжевых маркеров
    • Использование режима Assistant Mode

    Модуль 7. Проверка на соответствие MISRA-C

    Цель: использование Polyspace для проверки кода на соответствие MISRA-C.

    • Обзор стандарта написания кода MISRA-C
    • Запуск инструмента проверки на соответствие MISRA-C
    • Обзор результатов работы инструмента
    • Влияние верификации MISRA-C на Polyspace

    Модуль 8. Метрики и отчеты для представления в сети

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

    • Результаты предоставления общего доступа
    • Использование веб-метрики
    • Проверка требований к качеству
    • Создание документации

    Модуль 9. Контекстная верификация

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

    • Настройка контекстной верификации
    • Улучшение результатов контекстной верификации
    • Сравнение робастности и контекстной верификации


    Заявка на тренинг
    Связанные материалы