Exponenta Banner

polyspaceAutosar

Запустите Polyspace Code Prover на реализации кода компонентов программного обеспечения AUTOSAR с помощью скриптов MATLAB

свернуть все на странице

Синтаксис

[status, msg] = polyspaceAutosar('-create-project',projectFolder,'-arxml-dir',arxmlFolder,'-sources-dir',codeFolder,options)
[status, msg] = polyspaceAutosar('-update-project',prevProjectFile,options)
[status, msg] = polyspaceAutosar('-update-and-clean-project',prevProjectFile,options)
[status, msg, out] = polyspaceAutosar(___)

Описание

пример

[status, msg] = polyspaceAutosar('-create-project',projectFolder,'-arxml-dir',arxmlFolder,'-sources-dir',codeFolder,options) проверяет реализацию кода компонентов программного обеспечения AUTOSAR для ошибок времени выполнения и нарушения ограничений данных в соответствующих спецификациях XML AUTOSAR. Анализ анализирует спецификации XML AUTOSAR (.arxml файлы) в arxmlFolder, строит реализацию кода из модулей (.c файлы) в codeFolder на основе технических требований и Программы автоматического доказательства запусков Кода на каждом модуле для проверок. Результаты Программы автоматического доказательства Кода хранятся в projectFolder. После анализа можно открыть проект psar_project.psprj от projectFolder в пользовательском интерфейсе Polyspace® или файле psar_project.xhtml в веб-браузере. Можно просмотреть результаты для каждого компонента программного обеспечения индивидуально.

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

[status, msg] = polyspaceAutosar('-update-project',prevProjectFile,options) обновляет результаты анализа Программы автоматического доказательства Кода на основе изменений в файлах ARXML или исходном коде C начиная с последнего анализа. Обновление использует файл XHTML prevProjectFile от предыдущего анализа и повторно анализирует только реализацию кода компонентов программного обеспечения, которые изменились начиная с того анализа.

Можно использовать дополнительные опции для поиска и устранения неисправностей.

[status, msg] = polyspaceAutosar('-update-and-clean-project',prevProjectFile,options) обновляет результаты анализа Программы автоматического доказательства Кода на основе изменений в файлах ARXML или исходном коде C начиная с последнего анализа. Обновление повторно анализирует только реализацию кода компонентов программного обеспечения, которые изменились начиная с предыдущего анализа. Чистое обновление также удаляет информацию о компонентах программного обеспечения, которые устарели. Например, если вы используете дополнительную опцию обеспечить обновление для определенных компонентов программного обеспечения, и другие SWC-s также изменились, чистое обновление удаляет те другие SWC-s из проекта Polyspace.

Можно использовать дополнительные опции для поиска и устранения неисправностей.

[status, msg, out] = polyspaceAutosar(___) запускает анализ Программы автоматического доказательства Кода с помощью тех же опций как прежде. Выход, вместо того, чтобы появиться в Командном окне MATLAB®, перенаправляется к вектору символов out.

Примечание

Прежде чем вы запустите Polyspace из MATLAB, необходимо соединить Polyspace и установки MATLAB. Смотрите Интегрируют Серверные продукты Polyspace с MATLAB и Simulink.

Примеры

свернуть все

Предположим, что ваши файлы ARXML находятся в папке arxml и ваши исходные файлы C в папке code в текущей папке.

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

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

exampleDir = fullfile(polyspaceroot,'help',...
    'toolbox','codeprover','examples','polyspace_autosar');
arxmlDir = fullfile(exampleDir, 'arxml');
sourceDir = fullfile(exampleDir, 'code');

tempDir = tempdir;
projectDir = fullfile(tempDir, 'polyspace-project');
prevProjectFile = fullfile(projectDir, 'psar_project.xhtml');

% Update project file if it already exists, else create new project
projectDirAlreadyExists = isfolder(projectDir);

if projectDirAlreadyExists
    [status, msg] = polyspaceAutosar('-update-project', ...
        prevProjectFile);
else
    [status, msg] = polyspaceAutosar('-create-project', projectDir, ...
    '-arxml-dir', arxmlDir, ...
    '-sources-dir', sourceDir);
end

Входные параметры

свернуть все

Имя папки в виде вектора символов. Если папка существует, это должно быть пусто.

Пример: 'C:\Polyspace_Projects\proj_swc1'

Имя папки в виде вектора символов.

Пути UNC не поддержаны для имени папки.

Пример: 'C:\arxml_swc1'

Имя папки в виде вектора символов.

Пути UNC не поддержаны для имени папки.

Пример: 'C:\code_swc1'

Путь к ранее созданному файлу проекта psar_project.xhtmlВ виде вектора символов.

Пример: 'C:\Polyspace_Projects\proj1\psar_project.xhtml'

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

Задайте каждую опцию как вектор символов, сопровождаемый значением опции как отдельный вектор символов. Например, можно задать файл опций opts.txt при помощи синтаксиса polyspaceAutosar(...,'-options-file','opts.txt').

Общие опции

ОпцияЗначениеОписание
'-verbose' 

Сохраните дополнительную информацию о различных фазах выполнения команды (многословный режим). Файл psar_project.log и другие вспомогательные файлы хранят эту дополнительную информацию.

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

'-options-file'Имя файла опций, например, 'opts.txt'.

Используйте файл опций, чтобы добавить или заменить параметры командной строки. В файле опций задайте каждую опцию на отдельной линии. Начните линию с # указать на комментарии.

Файл опций opts.txt может выглядеть так:

# Store Polyspace results
-create-project polyspace
# ARXML Folder
-arxml-dir arxml
# SOURCE Folder
-sources-dir code

Если опция, которая непосредственно задана с polyspaceAutosar функционируйте конфликты с опцией в файле опций, непосредственно заданная опция используется.

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

Опции, чтобы управлять обновлением проекта

Если вы обновляете проект, по умолчанию, результаты анализа обновляются для всех поведений AUTOSAR SWC относительно любого изменения в файлах ARXML или исходном коде C начиная с последнего анализа. Управляйте обновлением при помощи этих опций.

ОпцияЗначениеОписание
'-autosar-behavior'Полное полностью определенное имя поведения SWC, например, 'pkg.component.bhv'.

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

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

Например:

  • Задавать компонент программного обеспечения, внутреннее поведение которого имеет полностью определенное имя pkg.component.bhvИспользование:

    polyspaceAutosar(...,
'-autosar-behavior',...
'pkg.component.bhv')

  • Задавать компоненты программного обеспечения, внутренние поведения которых полностью определили имена, начинающиеся с pkg.componentИспользование:

    polyspaceAutosar(...,
'-autosar-behavior',...
'pkg.component\..*')
    \. представляет диафрагму имени пакета . (точка) и .* представляет любое количество символов.

'-do-not-update-autosar-prove-environment' 

Не читайте технические требования ARXML. Используйте технические требования ARXML, сохраненные от предыдущего анализа.

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

'-do-not-update-extract-code' 

Не читайте исходный код C. Используйте исходный код, сохраненный от предыдущего анализа.

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

'-do-not-update-verification' 

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

Используйте эту опцию во время обновлений проекта, чтобы исследовать ошибки, введенные в технических требованиях ARXML или ошибках компиляции, введенных в исходном коде. Можно сначала устранить эти проблемы, и затем запустить анализ Программы автоматического доказательства Кода.

Опции, чтобы управлять парсингом технических требований ARXML

ОпцияЗначениеОписание
'-autosar-datatype'Полное полностью определенное имя типа данных, например, 'pkg.datatypes.type'

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

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

Например:

  • Задавать тип данных, который имеет полностью определенное имя pkg.datatypes.typeИспользование:

    polyspaceAutosar(...,
'-autosar-datatype',...
'pkg.datatypes.type')

  • Задавать типы данных, которые полностью определили имена, начинающиеся с pkg.datatypesИспользование:

    polyspaceAutosar(...,
'-autosar-datatype',...
'pkg.datatypes\..*')
    \. представляет диафрагму имени пакета . (точка) и .* представляет любое количество символов.

  • Чтобы обеспечить импорт всех типов данных, используйте:

    polyspaceAutosar(...,
'-autosar-datatype',...
'.*\..*')

'-Eautosar-xmlReaderSameUuidForDifferentElements'

'-Eno-autosar-xmlReaderSameUuidForDifferentElements'

 

Если несколько элементов в технических требованиях ARXML имеют тот же универсальный уникальный идентификатор (UUID), используйте эти опции, чтобы переключиться между предупреждением и ошибкой.

Анализ по умолчанию останавливается с ошибкой, если эта проблема происходит. Чтобы преобразовать в предупреждение, используйте '-Eno-autosar-xmlReaderSameUuidForDifferentElements'. Для конфликта UUIDs анализ хранит последнее чтение элемента и продолжает предупреждение.

Последующее выполнение продолжает использовать режим предупреждения. Чтобы вернуться назад к ошибке, используйте '-Eautosar-xmlReaderSameUuidForDifferentElements'.

'-Eautosar-xmlReaderTooManyUuids'

'-Eno-autosar-xmlReaderTooManyUuids'

 

Если тот же элемент в технических требованиях ARXML имеет различные универсальные уникальные идентификаторы (UUID), используйте эти опции, чтобы переключиться между предупреждением и ошибкой.

Анализ по умолчанию останавливается с ошибкой, если эта проблема происходит. Чтобы преобразовать в предупреждение, используйте '-Eno-autosar-xmlReaderTooManyUuids'. Для конфликта UUIDs анализ хранит последнее чтение элемента и продолжает предупреждение.

Последующее выполнение продолжает использовать режим предупреждения. Чтобы вернуться назад к ошибке, используйте '-Eautosar-xmlReaderTooManyUuids'.

Опции, чтобы управлять чтением исходного кода C

ОпцияЗначениеОписание
'-include'Файл с определениями типов и макроопределениями.

Задайте дополнительные типы данных и макросы, которые не являются частью ваших технических требований ARXML, но необходимый для анализа реализации кода.

Добавьте определения типов и макроопределения к файлу. Эти определения добавлены к заголовочному файлу Rte_Type.h это используется в анализе. Файл, который вы обеспечиваете, нельзя самостоятельно назвать Rte_Type.h.

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

Если вы дополнительно задаете макросы или не задаете их использующий опции '-D' или '-U', для определений, которые конфликтуют с теми в USER_RTE_TYPE_H, -D или -U технические требования преобладают.

'-I'Папка, содержащая заголовочные файлы.

Задайте папки, содержащие заголовочные файлы. Анализ ищет #include- d файлы в этой папке. Папка должна быть подпапкой вашей папки исходного кода.

Повторите опцию для нескольких папок. Анализ ищет заголовочные файлы в этих папках в порядке, в котором вы задаете их.

Если вы хотите задать папки, которые не находятся в папке исходного кода, используют опцию:

polyspaceAutosar(...,
 '-extra-project-options','-I INCLUDE_FOLDER')

'-D'Имя макроса, например, '_WIN32.

Задайте макросы, которые анализ должен рассмотреть, как задано.

Например, если вы задаете:

polyspaceAutosar(...,
 '-D','_WIN32')
условное выражение препроцессора #ifdef _WIN32 успешно выполняется и соответствующая ветвь выполняется.

'-U'Имя макроса, например, '_WIN32.

Задайте макросы, которые анализ должен рассмотреть как неопределенные.

Например, если вы задаете:

polyspaceAutosar(...,
 '-U','_WIN32')
условное выражение препроцессора #ifndef _WIN32 успешно выполняется и соответствующая ветвь выполняется.

Опции к проверкам Программы автоматического доказательства кода системы управления

ОпцияЗначениеОписание
'-extra-project-options'Разделенный пробелом список опций.

Задайте дополнительные опции для анализа Программы автоматического доказательства Кода. Опции, которые вы задаете, не применяются к парсингу ARXML или экстракции кода, но только к последующему анализу Программы автоматического доказательства Кода.

Используйте этот метод, чтобы задать аналитические опции, которые используются в non-AUTOSAR анализе Программы автоматического доказательства Кода. См. Аналитические Опции.

Например, вы можете хотеть задать компилятор и целевую архитектуру. По умолчанию компиляция проектов, созданных из технических требований AUTOSAR, использует gnu4.7 компилятор и i386 архитектуру.

Чтобы задать visual11.0 компилятор с x86_64 архитектурой, введите эту опцию:

polyspaceAutosar(...,
 '-extra-project-options','-compiler visual11.0 -target x86_64')
См. также Compiler (-compiler) и Target processor type (-target).

'-extra-options-file'Файл с опциями Polyspace.

Задайте дополнительные опции для анализа Программы автоматического доказательства Кода в файле опций. Опции, которые вы задаете, не применяются к парсингу ARXML или экстракции кода, но только к последующему анализу Программы автоматического доказательства Кода.

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

  1. Проследите свою команду сборки (например, make) с polyspaceConfigure функционируйте и сгенерируйте файл опций для последующего анализа Программы автоматического доказательства Кода. Подавите включение источников в файле опций с -no-sources опция.

    polyspaceConfigure -output-options-file options.txt -no-sources make

  2. Запустите Программу автоматического доказательства Кода на коде AUTOSAR с polyspace-autosar. Обеспечьте свою папку ARXML, исходные папки и другие опции. Кроме того, предоставьте ранее сгенерированному файлу опций -extra-options-file опция.

    polyspaceAutosar(...,
 '-extra-options-file','options.txt')

'-show-prove'Полное полностью определенное имя поведения SWC, например, 'pkg.component.bhv'.

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

Выходные аргументы

свернуть все

Булев флаг, указывающий, выполнение ли анализ до завершения. Если анализ завершается, возвращаемое значение 0, в противном случае это - ненулевое значение.

Если вы видите ненулевое значение, проверяйте второй выходной аргумент polyspaceAutosar для сообщений об ошибке.

Можно также искать сообщения об ошибке в файле psar_project.xhtml в вашей папке проекта. Можно использовать этот файл XHTML, чтобы определить, какие компоненты программного обеспечения анализировались.

Аналитический журнал в виде структуры с этими полями:

Тип сообщения, возвращенного как один из трех векторов символов:

  • 'info': Информация, такая как текущий этап анализа.

  • 'warning': Предупреждения, которые не останавливают анализ, но могут вызвать ошибки позже.

  • 'error': Ошибки, которые могут остановить целый анализ или анализ определенных компонентов программного обеспечения.

Чтобы проверить ошибки, используйте эту информацию о типе. Например, чтобы проверить ошибки в структуре в msg, используйте этот код:

% Convert to table for logical indexing
msgTable = struct2table(msg);

% Check which messages have the type 'error'
errorMatches = (strcmp(msgTable.Criticity, 'error'));

% Read the error messages to another table
errorMessage = msgTable(errorMatches, :);

Содержимое сообщения, возвращенного как вектор символов.

Пример: 'Start Extract user-implementation for Behavior ''pkg.tst002.swc001.bhv001''...'

Аналитический журнал, возвращенный как вектор символов.

Смотрите также

Темы

Введенный в R2018b

Документация Polyspace Code Prover Server
Поддержка