После анализа, 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 отчета перечисляет следующую информацию:
Имя модели
Релиз MATLAB, в котором выполнялся анализ
Значение контрольной суммы, которое представляет состояние анализируемой модели
Режим Analysis
Представление модели
Цель генерации тестов (применимый для анализа генерации теста)
Состояние Analysis
Предварительная обработка времени
Аналитическое время
Состояние целей анализируется. Это включает количество процента для каждого состояния
Глава Analysis Information отчета включает следующие разделы:
Раздел Model Information предоставляет следующую информацию о текущей версии модели:
Путь и имя файла модели, что Simulink Design Verifier анализируется
Версия модели
Дата и время, что модель была в последний раз сохранена
Имя человека, кто продержался сохраненный модель
Раздел Analysis Options предоставляет информацию об аналитических настройках Simulink Design Verifier.
Раздел Analysis Options перечисляет параметры, которые влияли на анализ Simulink Design Verifier. Если вы включили фильтрацию покрытия, имя файла фильтра включено в этот раздел.
Примечание
Для получения дополнительной информации об этих параметрах, см. Опции Simulink Design Verifier.
Если ваша модель включает неподдерживаемые блоки, по умолчанию, автоматическому блокированию позволяют позволить анализу продолжать. С автоматическим включенным блокированием программное обеспечение рассматривает только интерфейс неподдерживаемых блоков, не их фактическое поведение. Этот метод позволяет программному обеспечению завершать анализ. Однако анализ может достигнуть только частичных результатов, если какой-либо из неподдерживаемых блоков модели влияет на результат симуляции.
Раздел Unsupported Blocks появляется, только если анализ заблокировал неподдерживаемые блоки; это перечисляет неподдерживаемые блоки в таблице с гиперссылкой на каждый блок в модели.
Для получения дополнительной информации об автоматическом блокировании, смотрите Несовместимости Указателя с Автоматическим Блокированием.
Раздел User Artifacts предоставляет информацию о тестовых данных и данных о покрытии в анализе Simulink Design Verifier.
Раздел 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 аналитического отчета приводит эти границы.
Если блок Observer Reference будет использоваться в анализе поиска ошибок проектирования, то этот раздел покажет информацию о наблюдателе в подразделе Observer Model (s) и информацию о модели проекта в подразделе Design Model.
Таблица в подразделе Модели проекта показывает список каждой выведенной области значений в sldvdemo_debounce_validprop модель в качестве примера.
Раздел модели (моделей) The Observer не покажет выведенные области значений, о которых сообщают, когда наблюдатели проигнорированы для анализа поиска ошибок проектирования.
Этот раздел отчета предоставляет информацию обо всех целях в модели, включая тип цели, элемент модели, который соответствует типу и объективному описанию.
Программное обеспечение идентифицирует присутствие приближений и сообщает о них на уровне каждого объективного состояния. Для получения дополнительной информации смотрите Приближения Создания отчетов Через Результаты Валидации. Эта таблица суммирует объективное состояние для аналитических режимов Simulink Design Verifier.
| Аналитический режим | Объективное состояние |
|---|---|
|
Поиск ошибок проектирования |
|
|
Генерация тестов |
|
|
Доказательство свойства |
|
Если при запуске анализ поиска ошибок проектирования, раздел Design Error Detection Objectives Status может включать следующие объективные состояния:
Если блок Observer Reference будет использоваться в анализе поиска ошибок проектирования, то этот раздел покажет информацию о наблюдателе в подразделе Observer Model(s) и информацию о модели проекта в подразделе Design Model. Этот раздел будет пуст, когда не будет никакой активной логики, существующей в модели.
Таблица в подразделе Модели проекта показывает список активной логики в sldvdemo_debounce_validprop модель в качестве примера.
Раздел модели (моделей) The Observer не покажет активной логики, о которой сообщают, когда наблюдатели проигнорированы для анализа поиска ошибок проектирования.
Мертвая логика. Раздел 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.
Если блок Observer Reference будет использоваться в анализе генерации теста, то каждый раздел состояния цели тестирования покажет информацию о наблюдателе в подразделе Observer Model(s) информация о модели проекта в подразделе Design Model. Эти подразделы будут пусты, если никакая цель тестирования не нашла в модели.
Таблица показывает часть целей тестирования Objectives Satisfied для режима проектирования в sldvdemo_debounce_testobjblks модель в качестве примера.
Таблица показывает часть целей тестирования Objectives Satisfied для модели наблюдателя в sldvdemo_debounce_testobjblks модель в качестве примера.
Удовлетворенные цели. Раздел 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 может включать:
Если блок Observer Reference будет использоваться в доказывающем свойство анализе, то каждый раздел состояния цели доказательства покажет информацию о наблюдателе в подразделе Observer Model(s) и информацию о модели проекта в подразделе Design Model. Эти подразделы будут пусты, когда никакая цель не будет найдена в модели.
Таблица показывает цели доказательства Objectives Valid для модели The Observer в sldvdemo_debounce_validprop модель в качестве примера.
Допустимые цели. Раздел 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 в верхнем левом углу таблицы; программное обеспечение открывает новое окно, которое отображает объект подробно. Чтобы посмотреть детали теста, который был применен к определенной цели, кликните по номеру теста в последнем столбце таблицы.
Если блок Observer Reference будет использоваться в доказывающем свойство анализе, то каждый раздел элемента модели покажет информацию о наблюдателе в подразделе Observer Model(s) информация о модели проекта в подразделе Design Model. Эти подразделы будут пусты, если никакая цель тестирования не нашла в модели.
Таблица показывает одну из целей тестирования для модели проекта в sldvdemo_debounce_testobjblks модель в качестве примера.
Таблица показывает одну из целей тестирования для модели наблюдателя в sldvdemo_debounce_testobjblks модель в качестве примера.
Если вы выполняете анализ поиска ошибок проектирования, и анализ обнаруживает ошибки проектирования в модели, отчет включает в себя главу 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. Эта глава включает разделы, которые обобщают цели доказательства и любые контрпримеры сгенерированное программное обеспечение:
Глава Свойств содержит оглавление. Каждый элемент в оглавлении является гиперссылкой на информацию об определенном свойстве, которое было сфальсифицировано.
Если блок Observer Reference будет использоваться в доказывающем свойство анализе, то каждая глава свойств покажет информацию о наблюдателе в подразделе Observer Model(s) информация о модели проекта в подразделе Design Model. Это будет пусто, когда не будет никаких свойств в модели.
Таблица показывает одно из свойств для модели наблюдателя в sldvdemo_debounce_validprop модель в качестве примера.
Списки разделов Summary:
Элемент модели, что программное обеспечение анализируется
Тип свойства, которое было оценено
Состояние анализа
В следующем примере программное обеспечение анализировало sldvdemo_cruise_control_verification модель для доказательства свойства. Анализ доказал, что вход с блоком Assertion под названием BrakeAssertion был ненулевым.
Раздел Counterexample перечисляет временной шаг и соответствующее время, в которое контрпример сфальсифицировал свойство. Этот раздел также перечисляет значения сигналов, в то время продвигаются.
