Просмотр результатов Polyspace на коде AUTOSAR

В этом разделе описывается основанный на компонентах подход к проверке кода AUTOSAR с Polyspace. Для подхода интегрирования анализа смотрите Выбор между основанным на компонентах и Интегрировании анализом кода AUTOSAR с Polyspace.

Это руководство описывает, как открыть Polyspace®Результаты Code Prover™ для специфичного для AUTOSAR кода и интерпретации результатов, которые подчеркивают нарушение ограничений данных в ARXML.

Code Prover проверяет реализацию кода программных компонентов AUTOSAR на несоответствие спецификациям в ARXML. Например, если аргумент функции RTE имеет значение, выходящей за пределы ограниченной области значений, заданного в ARXML, анализ помечает возможную проблему.

Чтобы следовать шагам в этом руководстве, запустите Polyspace на демо- файлы в polyspaceroot\ help\toolbox\codeprover\examples\polyspace _ авто-РСА. Используйте приведенную в этом руководстве информацию для просмотра конкретных результатов AUTOSAR. Для получения справки по выполнению анализа смотрите Run Polyspace on AUTOSAR Code.

Открытые результаты

Если вы запускаете анализ в пользовательском интерфейсе Polyspace, можно открыть каждый результат непосредственно. Дважды кликните результат, который необходимо открыть.

Если вы запускаете анализ с помощью скриптов, после анализа можно открыть результаты несколькими способами.

  • Откройте файл psar_project.xhtml из папки проекта в веб-браузере. Вы увидите обзор результатов для всех компонентов программного обеспечения и перейдите к результатам для каждого компонента программного обеспечения. Для получения дополнительной информации смотрите Обзор результатов для всех компонентов программного обеспечения.

  • Откройте файл psar_project.psprj из папки проекта в пользовательском интерфейсе Polyspace. Откройте каждый результат на панели Project Browser.

  • Перейдите к папкам, содержащим отдельные файлы результатов. Откройте файл результата (с расширением .pscp) в пользовательском интерфейсе Polyspace.

    Файлы результатов хранятся в подпапке AUTOSAR папки проекта. Путь к каждому результату следует за полным именем внутреннего поведения программного компонента. Например, для полного имени pkg.component.bhv, результаты хранятся в AUTOSAR\pkg\component\bhv\verification (имя конечной подпапки CP_Result при запуске верификации в пользовательском интерфейсе Polyspace).

См. обзор результатов для всех программных компонентов

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

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

В файл psar_project.xhtmlщелкните значок в верхнем левом углу. На левой панели нажмите кнопку Behaviors. Вы можете увидеть список всех программных компонентов, чье внутреннее поведение извлечено.

Можно фильтровать этот список, чтобы отобразить только интересующие вас программные компоненты. Чтобы увидеть определенные программные компоненты, в поле поиска введите полное имя интересующего вас программного компонента.

Можно также вводить регулярные выражения для просмотра нескольких компонентов. Например, чтобы увидеть все компоненты, чьи квалифицированные имена начинаются с pkg.tst002.swc001, введите выражение:

^pkg.tst002.swc001.*

Нажмите Search. В списке справа отображаются только запрошенные компоненты программного обеспечения.

Можно также отфильтровать компоненты на основе других критериев:

  • Успех или отказ верификации

    Чтобы просмотреть только программные компоненты, завершившие верификацию, щелкните и очистите error status фильтр.

  • Наличие или отсутствие определенных видов результатов, для образца, красных проверок

    Чтобы просмотреть только программные компоненты, которые имеют красные проверки, щелкните все в строке, содержащей red фильтр, кроме самого red фильтра.

Смотрите исполняемые и исходные файлы в программном компоненте

Для каждого программного компонента вы можете увидеть эту информацию в файле psar_project.xhtml в папке проекта (см. предыдущий рисунок).

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

    Чтобы убедиться, что анализ Code Prover был завершен, в разделе Verification of extracted implementation code, проверьте этот оператора:

    State after last command execution: updated.

  • Функции, предоставляемые этим программным компонентом и Rte_ используемые функции.

    Чтобы просмотреть этот список, щелкните ссылку:

    See key autosar definition for this behavior

  • Графическое представление runnables в программном компоненте. Графическое представление показывает:

    • Функции точки входа, реализующие runnables и их callees

    • Файлы, содержащие эти функции

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

    В этом примере вы видите, что программный компонент с внутренним поведением bhv001 имеет три выполняемые функции, реализованные через функции точки входа foo, init, и step. Все три функции точки входа определены в файле swc001.c.

    Функция step вызывает функции, определенные в других файлах, например dep3.c. Вы можете кликнуть значок для step просматривать только файлы, участвующие в реализации step runnable. Чтобы вернуться к полному графическому представлению программного компонента, щелкните в любом месте пустого пространства на графике.

  • Обзор результатов Code Prover со ссылками на файлы результатов.

    Проверьте такие линии, как эти линии:

    Verification results are in summary: green check=84, orange check=2, red check=1
    Щелкните ссылку, следующую за линией, чтобы открыть файл результатов в пользовательском интерфейсе Polyspace. Если вы еще не открыли .pscp ранее, нажав ссылку, можно просто загрузить файл результатов. Убедитесь, что .pscp файлы всегда открываются в пользовательском интерфейсе Polyspace (с исполняемым файлом polyspaceroot\ polyspace\bin, где polyspaceroot - папка установки Polyspace).

    Результаты состоят из специфичных для AUTOSAR проверок во время выполнения, таких как Invalid result of AUTOSAR runnable implementation и общие проверки во время выполнения C/C + +, такие как Division by zero.

Интерпретируйте проверки AUTOSAR во время выполнения для программного компонента

На панели Results List выберите результат Invalid result of AUTOSAR runnable implementation или Invalid use of AUTOSAR runtime environment function. Исследуйте результат далее с помощью информации на различных панелях.

Проверяйте возвращаемое значение и аргументы

Используя информацию на панели Result Details, определите, нарушает ли значение возврата или аргумент ограничения данных в ARXML или может иметь значение NULL. Ищите! значок, который указывает на определенную ошибку или? значок, указывающий на возможную ошибку.

Для значения возврата и каждого аргумента отображаются фактические возможные значения во время выполнения и значения, разрешенные типом данных в спецификации ARXML. Сравните их и найдите значение, которое не разрешено.

Результат Invalid result of AUTOSAR runnable implementation определяет, может ли возвращаемое значение функции, реализующей runnable, или выходных аргументов нарушить ограничения данных. Результат Invalid use of AUTOSAR runtime environment function определяет, являются ли входные параметры Rte_ функция нарушает ограничения данных.

Проверяйте спецификацию аргумента (необязательно)

Иногда может потребоваться отобразить тип данных приложения, из которого берётся переменный тип базового программного обеспечения. Щелкните синюю ссылку спецификации параметра и смотрите экстракт ARXML, который описывает эту информацию о типе данных параметра или возвращаемого значения:

  • Тип данных приложения, тип данных реализации и тип базового программного обеспечения

  • Ограничение данных, модуль и метод расчетов

Поиск первопричины результата

Исследуйте, как переменная получает значения, которые нарушают ограничения данных. Чтобы отследить код назад, на панели Source, щелкните правой кнопкой мыши переменную и найдите все ее образцы или перейдите к ее определению. Для получения дополнительной информации смотрите Результаты интерпретации Code Prover в Polyspace Desktop User Interface.

Решите, исправлять ли код или ARXML, или обосновать результат с помощью комментариев. Смотрите Адрес Результаты Polyspace через исправления ошибок или обоснования.

См. также

|

Похожие темы