Создайте аналитическую настройку Polyspace из технических требований AUTOSAR

Если вы используете методологию AUTOSAR для разработки программного обеспечения, можно создать аналитическую настройку Polyspace^® непосредственно из технических требований AUTOSAR. С продуктом, Polyspace Code Prover™ Server™, можно затем запустить анализ Программы автоматического доказательства Кода реализации кода Компонентов программного обеспечения AUTOSAR.

Чтобы выполнить шаги в этом примере, используйте демонстрационные файлы в polyspaceroot\help\toolbox\polyspace_code_prover_server\examples\polyspace_autosar.

Преимущества Polyspace для AUTOSAR

Polyspace для AUTOSAR запускает статический анализ программы реализации кода компонентов программного обеспечения AUTOSAR. Анализ ищет возможные ошибки времени выполнения или несоответствие с техническими требованиями в AUTOSAR XML (ARXML).

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

Несоответствие с техническими требованиями AUTOSAR: Эти проверки стремятся доказывать, что определенные функции реализуются или используются в соответствии с техническими требованиями в ARXML. Проверки применяются к runnables (функции, обеспеченные компонентами программного обеспечения) и к использованию функций, предоставленных Средой выполнения (RTE). Смотрите также:
- AUTOSAR runnable not implemented (Polyspace Code Prover Access)
- Invalid result of AUTOSAR runnable implementation (Polyspace Code Prover Access)
- Invalid use of AUTOSAR runtime environment function (Polyspace Code Prover Access)
Например, если аргумент функции RTE имеет значение вне ограниченной области значений, заданной в ARXML, анализ отмечает возможную проблему.
Ошибки времени выполнения: Эти проверки стремятся доказывать отсутствие определенных типов ошибок времени выполнения в телах runnables (например, переполнение). Доказательство использует технические требования в ARXML, чтобы определить точные области значений для выполнимых аргументов и возвращаемых значений функции RTE и выходных аргументов. Например, доказательство рассматривает только те значения выполнимых аргументов, которые заданы в их типах данных AUTOSAR.

Запустите Polyspace на коде AUTOSAR

Запуститесь polyspace-autosar команда с путями к вашему ARXML и папке исходного кода. Команда анализирует ARXML и исходные файлы, создает проект Polyspace и анализирует все модули в проекте для ошибок времени выполнения или нарушения ограничений данных в ARXML.

На первом показе задайте путь к своему ARXML и исходным файлам явным образом. В более поздних запусках задайте файл psar_project.xhtml созданный в предыдущем запуске. Анализ обнаруживает изменения в ARXML и исходных файлах начиная с последнего запуска и повторно анализирует только те модули где измененная реализация компонента программного обеспечения. Если спецификация ARXML изменилась начиная с предыдущего анализа новый анализ повторно анализирует все модули.

Например, можно запустить эти команды в .bat скрипт. На первом показе этот скрипт ищет технические требования ARXML в папке arxml в текущей папке и исходных файлах C в папке code. Результаты хранятся в папке polyspace в текущей папке. В более поздних запусках, аналитические повторные использования результат предыдущего пробегает файл psar_project.xhtml и обновляет результаты только для компонентов программного обеспечения, измененных начиная с последнего запуска.

echo off
set POLYSPACE_AUTOSAR_PATH=C:\Program Files\Polyspace Server\R2019a\polyspace\bin

IF NOT EXIST polyspace\psar_project.xhtml (
"%POLYSPACE_AUTOSAR_PATH%\polyspace-autosar" -create-project polyspace -arxml-dir arxml -sources-dir code
) ELSE (
"%POLYSPACE_AUTOSAR_PATH%\polyspace-autosar" -update-project polyspace\psar_project.xhtml
)
Pause

Можно также запустить Программу автоматического доказательства Кода на реализации кода компонентов программного обеспечения AUTOSAR со скриптами MATLAB^®. Смотрите polyspaceAutosar.

Загрузите результаты на Polyspace доступ к веб-интерфейсу

Для каждого поведения Компонента программного обеспечения анализ Программы автоматического доказательства Кода производит отдельный файл результата (с дополнительным .pscp). Путь к файлу результатов определяется полностью определенным именем Компонента программного обеспечения. Например:

Поведение Компонента программного обеспечения с полным именем pkg.tst002.swc001.bhv001 имеет результаты, сохраненные в файле ps_results.pscp в подпапке AUTOSAR\pkg\tst002\swc001\bhv001\verification\ из папки результатов.
Поведение Компонента программного обеспечения с полным именем pkg.tst002.swc002.bhv имеет результаты, сохраненные в файле ps_results.pscp в подпапке AUTOSAR\pkg\tst002\swc002\bhv\verification\ из папки результатов.

Чтобы загрузить все результаты, используйте polyspace-access команда. Перед использованием polyspace-access команда, необходимо записать некоторый дополнительный код, чтобы найти папки, непосредственно содержащие файл результатов. Также необходимо создать имя для каждого результата, как это появилось бы на Polyspace доступ к веб-интерфейсу (в противном случае, все загрузки используют то же имя по умолчанию и перезаписывают друг друга). Основной алгоритм следующий:

Рекурсивно ищите все подпапки папки результатов для файлов с дополнительным .pscp. Используйте подпуть к папке, который непосредственно содержит .pscp файл в качестве аргумента для -upload опция polyspace-access команда.
Создайте имя результата на основе пути от верхней части папки результатов к подпапке, непосредственно содержащей .pscp файл. Используйте это имя в качестве аргумента для -project опция polyspace-access команда.

Демонстрационный пакетный файл Windows^® для загрузки может выглядеть так:

echo off
setlocal enabledelayedexpansion
set POLYSPACE_AUTOSAR_PATH=C:\Program Files\Polyspace Server\R2019a\polyspace\bin

rem Recursively search for all files with extension .pscp
dir *.pscp /b /s > file.txt

rem Upload each result file to Polyspace Access web interface
for /f "delims=" %%g in (file.txt) do (
    rem Get full path to result file with extension .pscp, then remove trailing '\'
    set filePath=%%~dpg
    set filePath=!filePath:~0,-1!
    rem Remove the current folder from the full path, then replace '\' with '.', then remove leading '.'
    set projectName=!filePath:%cd%=!
    set projectName=!projectName:\=.!
    set projectName=!projectName:~1!
    polyspace-access login -parent-project autosar -upload "!filePath!" -project !projectName!
)

Pause

В этом скрипте, переменной login относится к следующей комбинации опций. Вы предоставляете эти возможности с каждым использованием polyspace-access команда.

-host hostName -port portNumber -login username -encrypted-password pwd

Здесь, hostName имя веб-сервера Polyspace Code Prover Access™. Для локально размещенного сервера используйте localhost. portNumber дополнительный номер порта сервера. Если вы не используете номер порта, 9443 используется. username и pwd обратитесь к входу в систему и зашифрованной версии вашего пароля. Создать зашифрованный пароль, введите:

polyspace-access -encrypt-password

Скопируйте зашифрованный пароль и предоставьте этому паролю более позднее использование polyspace-access команда.

Если результаты загружаются, вы видите их в Polyspace доступ к веб-интерфейсу. В предыдущем скрипте, название проекта autosar используется с опцией -parent-project для всех файлов результатов. После загрузки все результаты появляются в соответствии с этим родительским проектом.

Для получения дополнительной информации о том, как рассмотреть результаты, см. документацию Polyspace Code Prover Access.

Документация