Отчеты Simulink Design Verifier

Генерация отчета Simulink Design Verifier

После анализа Simulink® Design Verifier™ может сгенерировать отчет HTML, который содержит подробную информацию о результатах анализа.

Аналитический отчет содержит гиперссылки, которые позволяют вам:

  • Перейдите к определенной части отчета

  • Перейдите к объекту в вашей модели Simulink, для которой анализ записал результаты

Можно также сгенерировать дополнительную версию PDF отчета Simulink Design Verifier.

Создайте аналитические отчеты

Чтобы создать отчет детального анализа прежде или после анализа, выполнить одно из следующих действий:

  • Перед анализом, в диалоговом окне Configuration Parameters, на Design Verifier> панель Report, выбирают Generate report of the results. Если вы хотите сохранить дополнительную версию PDF отчета Simulink Design Verifier, выберите Generate additional report in PDF format.

  • После анализа, в Simulink Design Verifier регистрируют окно, можно выбрать HTML или формат PDF и Generate detailed analysis report.

Вступительная часть

Отчет начинается с двух разделов:

Заголовок

Раздел заголовка перечисляет следующую информацию:

  • Модель или подсистема называют Simulink Design Verifier анализируемым

  • Имя пользователя сопоставлено с текущим сеансом MATLAB®

  • Дата и время, что Simulink Design Verifier сгенерировал отчет

Оглавление

Оглавление следует за разделом заголовка. Нажатие на элементы в оглавлении позволяет вам перейти быстро к конкретным главам в отчете.

Итоговая глава

Глава Summary отчета перечисляет следующую информацию:

  • Имя модели

  • Режим Analysis

  • Представление модели

  • Состояние Analysis

  • Предварительная обработка времени

  • Аналитическое время

  • Состояние целей анализируется

Глава информации об анализе

Глава Analysis Information отчета включает следующие разделы:

Информация модели

Раздел Model Information предоставляет следующую информацию о текущей версии модели:

  • Путь и имя файла модели, что Simulink Design Verifier анализируется

  • Версия модели

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

  • Имя человека, кто продержался сохраненный модель

Аналитические опции

Раздел Analysis Options предоставляет информацию об аналитических настройках Simulink Design Verifier.

Раздел Analysis Options перечисляет параметры, которые влияли на анализ Simulink Design Verifier. Если вы включили фильтрацию покрытия, имя файла фильтра включено в этот раздел.

Примечание

Для получения дополнительной информации об этих параметрах, см. Опции Simulink Design Verifier.

Неподдерживаемые блоки

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

Раздел Unsupported Blocks появляется, только если анализ заблокировал неподдерживаемые блоки; это перечисляет неподдерживаемые блоки в таблице с гиперссылкой на каждый блок в модели.

Для получения дополнительной информации об автоматическом блокировании, смотрите Несовместимости Указателя с Автоматическим Блокированием.

Ограничения

Раздел Constraints предоставляет информацию об условиях испытания, которые применил Simulink Design Verifier, когда это анализировало модель.

Можно перейти к ограничению в модели путем нажатия на гиперссылку в таблице Constraints. Программное обеспечение подсвечивает соответствующий блок Test Condition в вашем окне модели и открывает новое окно, показывающее блок подробно.

Блокируйте заменяющие сводные данные

Заменяющие Сводные данные Блока предоставляют обзор замен блока что выполняемый Simulink Design Verifier. Это появляется, только если Simulink Design Verifier заменил блоки в модели.

Каждая строка таблицы соответствует конкретному заменяющему правилу блока, что Simulink Design Verifier применился к модели. Таблица приводит следующее:

  • Имя файла, который содержит заменяющее правило блока и значение BlockType параметр правило задает

  • Описание правила, что MaskDescription параметр заменяющего блока задает

  • Имена блоков, что Simulink Design Verifier заменяется в модели

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

Приближения

Каждая строка таблицы Approximations описывает определенный тип приближения, которое Simulink Design Verifier использовал во время его анализа модели.

Примечание

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

Выведенная глава областей значений

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

Таблица в главе Derived Ranges аналитического отчета приводит эти границы.

Главы состояния целей

Этот раздел отчета предоставляет информацию обо всех целях в модели, включая тип цели, элемент модели, который соответствует типу и объективному описанию.

Программное обеспечение идентифицирует присутствие приближений и сообщает о них на уровне каждого объективного состояния. Для получения дополнительной информации смотрите Приближения Создания отчетов Через Результаты Валидации. Эта таблица суммирует объективное состояние для аналитических режимов Simulink Design Verifier.

Аналитический режимОбъективное состояние

Поиск ошибок проектирования

Генерация тестов

Доказательство свойства

Состояние целей поиска ошибок проектирования

Если при запуске анализ поиска ошибок проектирования, раздел Design Error Detection Objectives Status может включать следующие объективные состояния:

Мертвая логика.  Раздел Dead Logic перечисляет элементы модели, для которых анализ нашел мертвую логику.

Это изображение показывает раздел Dead Logic сгенерированного аналитического отчета для sldvdemo_fuelsys_logic_simple модель.

Мертвая логика при Приближении.  Раздел Dead Logic under Approximation перечисляет элементы модели, для которых анализ нашел мертвую логику при ударе приближения.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Dead Logic.

Это изображение показывает раздел Dead Logic under Approximation сгенерированного аналитического отчета.

Активная Логика - Симуляция Потребностей.  Раздел Active Logic - Needs Simulation перечисляет элементы модели для который анализ, найденный активной логикой. Чтобы подтвердить активное логическое состояние, необходимо запустить дополнительные симуляции тестов.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Active Logic.

Это изображение показывает фрагмент раздела Active Logic - Needs Simulation сгенерированного аналитического отчета для sldvdemo_fuelsys_logic_simple модель.

Допустимые цели.  Раздел Objectives Valid перечисляет цели поиска ошибок проектирования что анализ, найденный допустимым. Для этих целей анализ решил, что описанные ошибки проектирования не могут произойти.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Proven Valid.

Это изображение показывает раздел Objectives Valid сгенерированного аналитического отчета для sldvdemo_design_error_detection модель.

Цели, Допустимые при Приближении.  Раздел Objectives Valid under Approximation перечисляет цели поиска ошибок проектирования что анализ, найденный допустимым при ударе приближения.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Proven Valid.

Это изображение показывает раздел Objectives Valid under Approximation сгенерированного аналитического отчета.

Сфальсифицированные цели - Симуляция Потребностей.  Раздел Objectives Falsified - Needs Simulation перечисляет цели поиска ошибок проектирования, для которых анализ нашел тесты, которые демонстрируют ошибки проектирования. Чтобы подтвердить сфальсифицированное состояние, необходимо запустить дополнительные симуляции тестов.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Falsified.

Это изображение показывает раздел Objectives Falsified - Needs Simulation сгенерированного аналитического отчета для sldvdemo_design_error_detection модель.

Состояние целей тестирования

Если при запуске анализ генерации теста, раздел Test Objectives Status может включать следующие объективные состояния:

Когда вы анализируете модель с набором Model coverage objectives к Enhanced MCDC, программное обеспечение сообщает о состоянии обнаружения элементов модели. Для получения дополнительной информации смотрите Расширенное Покрытие MCDC в Simulink Design Verifier.

Удовлетворенные цели.  Раздел Objectives Satisfied перечисляет цели тестирования что анализ, которому удовлетворяют. Сгенерированные тесты покрывают цели.

Это изображение показывает фрагмент раздела Objectives Satisfied сгенерированного аналитического отчета для sldvdemo_fuelsys_logic_simple модель в качестве примера.

Удовлетворенные цели - Симуляция Потребностей.  Раздел Objectives Satisfied - Needs Simulation перечисляет цели тестирования что анализ, которому удовлетворяют. Чтобы подтвердить состояние, которому удовлетворяют, необходимо запустить дополнительные симуляции тестов.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Satisfied.

Это изображение показывает раздел Objectives Satisfied - Needs Simulation сгенерированного аналитического отчета.

Невыполнимые цели.  Раздел Objectives Unsatisfiable перечисляет цели тестирования, что определенному анализу нельзя было удовлетворить.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Proven Unsatisfiable.

Это изображение показывает раздел Objectives Unsatisfiable сгенерированного аналитического отчета для sldvdemo_fuelsys_logic_simple модель в качестве примера.

Цели, Невыполнимые при Приближении.  Раздел Objectives Unsatisfiable under Approximation перечисляет цели тестирования, что определенному анализу нельзя было удовлетворить из-за приближения во время анализа.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Proven Unsatisfiable.

Это изображение показывает раздел Objectives Unsatisfiable under Approximation сгенерированного аналитического отчета.

Цели, Нерешенные с Тестовыми сценариями.  Раздел Objectives Undecided with Testcases перечисляет цели тестирования, которые не решены из-за удара приближения во время анализа.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Satisfied.

Это изображение показывает раздел Objectives Undecided with Testcases сгенерированного аналитического отчета для sldvApproximationsExample модель в качестве примера.

Состояние целей доказательства

Если при запуске доказывающий свойство анализ, раздел Proof Objectives Status может включать:

Допустимые цели.  Раздел Objectives Valid перечисляет цели доказательства что анализ, найденный допустимым.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Proven Valid.

Это изображение показывает раздел Objectives Valid сгенерированного аналитического отчета для sldvdemo_debounce_validprop модель в качестве примера.

Цели, Допустимые при Приближении.  Раздел Objectives Valid under Approximation перечисляет цели доказательства что анализ, найденный допустимым при ударе приближения.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Objectives Proven Valid.

Это изображение показывает раздел Objectives Valid under Approximation сгенерированного аналитического отчета.

Цели, Сфальсифицированные с Контрпримерами.  Раздел Objectives Falsified with Counterexamples перечисляет цели доказательства, которые опроверг анализ. Сгенерированный контрпример показывает нарушение цели доказательства.

Это изображение показывает раздел Objectives Falsified with Counterexamples сгенерированного аналитического отчета для sldvdemo_debounce_falseprop модель в качестве примера.

Сфальсифицированные цели - Симуляция Потребностей.  Раздел Objectives Falsified - Needs Simulation перечисляет цели доказательства, которые опроверг анализ. Чтобы подтвердить сфальсифицированное состояние, необходимо запустить дополнительные симуляции контрпримеров.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Objectives Falsified with Counterexamples.

Это изображение показывает раздел Objectives Falsified - Needs Simulation сгенерированного аналитического отчета.

Цели, Нерешенные с Контрпримерами.  Раздел Objectives Undecided with Counterexamples перечисляет цели доказательства, нерешенные из-за удара приближения во время анализа.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Falsified.

Это изображение показывает раздел Objectives Undecided with Counterexamples сгенерированного аналитического отчета.

Цели, Нерешенные из-за Ошибки периода выполнения

Для целей доказательства и целей тестирования, раздел Objectives Undecided due to Runtime Error перечисляет нерешенные цели во время анализа из-за ошибки времени выполнения. Ошибка времени выполнения произошла в процессе моделирования теста или контрпримера.

В релизах перед R2017b этот раздел может включать цели, которые были отмечены как Falsified или Satisfied.

Это изображение показывает раздел Objectives Undecided due to Runtime Error сгенерированного аналитического отчета.

Цели, нерешенные из-за деления на нуль

Для всех типов целей раздел Objectives Undecided Due to Division by Zero перечисляет нерешенные цели во время анализа из-за ошибок деления на нуль в связанных элементах модели. Чтобы обнаружить ошибки деления на нуль прежде, чем запустить последующий анализ на вашей модели, выполните процедуру в, Обнаруживают Ошибки Целочисленного переполнения и Деления на нуль.

Цели, нерешенные из-за нелинейности

Для всех типов целей раздел Objectives Undecided Due to Nonlinearities перечисляет нерешенные цели во время анализа из-за необходимого расчета нелинейной арифметики. Simulink Design Verifier не поддерживает нелинейную арифметическую или нелинейную логику.

Цели, нерешенные из-за блокирования

Для всех типов целей раздел Objectives Undecided Due to Stubbing перечисляет элементы модели с нерешенными целями во время анализа из-за блокирования. В релизах перед R2013b эти цели могут включать цели, которые были отмечены как Objectives Satisfied – No Test Case или Objectives Falsified – No Counterexample.

Цели, нерешенные из-за массива за пределы

Для всех типов целей раздел Objectives Undecided Due to Array Out of Bounds перечисляет нерешенные цели во время анализа из-за массива за пределы ошибки в связанных элементах модели. Чтобы обнаружить за пределы ошибки массивов в вашей модели, смотрите, Обнаруживают Из Связанных Ошибок Доступа к массиву.

Нерешенные цели

Для всех типов целей раздел Objectives Undecided перечисляет цели, для которых анализ не мог определить результат в выделенное время.

В этом доказывающем свойство примере любой программное обеспечение превысило свое аналитическое ограничение по времени (который параметр Maximum analysis time задает), или вы прервали анализ, прежде чем это завершило обработку этих целей.

Глава элементов модели

Глава Model Items отчета включает таблицу для каждого объекта в модели, которая задает цели покрытия. Таблица для детали списки объектов все связанные цели, объективные типы, объективные описания и состояние каждой цели в конце анализа.

Таблица для отдельного объекта в модели выглядит похожей на этого для Интегратора Дискретного времени в подсистеме ПИ-контроллера sldvdemo_cruise_control модель в качестве примера.

Чтобы подсветить данный объект в вашей модели, нажмите View в верхнем левом углу таблицы; программное обеспечение открывает новое окно, которое отображает объект подробно. Чтобы посмотреть детали теста, который был применен к определенной цели, кликните по номеру теста в последнем столбце таблицы.

Глава ошибок проектирования

Если вы выполняете анализ поиска ошибок проектирования, и анализ обнаруживает ошибки проектирования в модели, отчет включает в себя главу Design Errors. Эта глава обобщает ошибки проектирования, которые сфальсифицировал анализ:

Оглавление

Каждая глава Ошибок проектирования содержит оглавление. Каждый элемент в оглавлении является гиперссылкой на результаты об определенной ошибке проектирования.

Сводные данные

Списки разделов Summary:

  • Элемент модели

  • Тип ошибки проектирования, которая была обнаружена (переполнение или деление на нуль)

  • Состояние анализа (Сфальсифицированный или Доказанный Допустимый)

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

Тест

Раздел Test Case перечисляет временной шаг и соответствующее время, в которое тест сфальсифицировал цель ошибки проектирования. Блок Inport raw имел значение 255, который вызвал ошибку переполнения.

Глава тестов

Если при запуске анализ генерации тестов, отчет включает в себя главу Test Cases. Эта глава включает разделы, которые обобщают тесты сгенерированный анализ:

Оглавление

Каждая глава Тестов содержит оглавление. Каждый элемент в оглавлении является гиперссылкой на информацию об определенном тесте.

Сводные данные

Списки разделов Summary:

  • Длина сигналов, которые включают тест

  • Общее количество целей тестирования, которых достигает тест

Цели

Списки разделов Objectives:

  • Временной шаг, на котором тест достигает той цели.

  • Время, в которое тест достигает той цели.

  • Ссылка на элемент модели сопоставлена с той целью. Нажатие на ссылку подсвечивает элемент модели в Редакторе Simulink.

  • Цель, которая была достигнута.

Сгенерированные входные данные

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

Примечание

Сгенерированная Таблица входных данных отображает тире (–) вместо номера как значение сигналов, когда значение сигнала в то время шаг не влияет на цель тестирования. В модели тестовой обвязки блок Inputs представляет эти значения с нулями, если вы не включаете параметр Randomize data that does not affect outcome (см., Рандомизируют данные, которые не влияют на результат).

Ожидаемый Выход

Если вы выбираете Include expected output values на Design Verifier> панель Results диалогового окна Configuration Parameters, отчет включает в себя раздел Expected Output для каждого теста. Для каждого выходного сигнала, сопоставленного с элементом модели, эта таблица приводит ожидаемое выходное значение на каждом временном шаге.

Объединенные цели

Если вы устанавливаете опцию Test suite optimization на CombinedObjectives (значение по умолчанию), глава Тестов может включать отдельную информацию о многих тестах.

Длинные тесты

Если вы устанавливаете опцию Test suite optimization на LongTestcases, глава Тестов в отчете включает меньше разделов о более длинных тестах.

Глава свойств

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

Оглавление

Каждая глава Свойств содержит оглавление. Каждый элемент в оглавлении является гиперссылкой на информацию об определенном свойстве, которое было сфальсифицировано.

Сводные данные

Списки разделов Summary:

  • Элемент модели, что программное обеспечение анализируется

  • Тип свойства, которое было оценено

  • Состояние анализа

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

Контрпример

Раздел Counterexample перечисляет временной шаг и соответствующее время, в которое контрпример сфальсифицировал свойство. Этот раздел также перечисляет значения сигналов, в то время продвигаются.

Документация Simulink Design Verifier
Поддержка
Для просмотра документации необходимо авторизоваться на сайте