Отчеты Simulink Design Verifier
Simulink Design Verifier
После анализа Simulink® Design Verifier™ может сгенерировать HTML, содержащий подробную информацию о результатах анализа.
Отчет об анализе содержит гиперссылки, которые позволяют:
Перейдите к определенной части отчета
Перейдите к объекту в модели Simulink, для которого анализ записал результаты
Можно также сгенерировать дополнительный PDF отчета Simulink Design Verifier.
Создание отчетов об анализе
Чтобы создать детальный анализ отчет до или после анализа, выполните одно из следующих действий:
Перед анализом в диалоговом окне Параметры конфигурации на панели 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
Таблица
Содержание таблицы в соответствии с разделом title. Нажатие элементов в таблицу содержимого позволяет быстро перемещаться к конкретным главам в отчете.
Сводная глава
В Summary главе отчета приводится следующая информация:
Имя модели
MATLAB release, в котором был выполнен анализ
Значение контрольной суммы, которое представляет состояние анализируемой модели
Режим анализа
Представление модели
Цель генерации теста (применяется для анализа генерации тестового примера)
Статус анализа
Время предварительной обработки
Время анализа
Состояние проанализированных целей. Это включает процентное число для каждого статуса
Глава «Информация об анализе»
В Analysis Information главе доклада содержатся следующие разделы:
Информация о модели
Раздел Model Information предоставляет следующую информацию о текущей версии модели:
Путь и имя файла модели, которую анализировал Simulink Design Verifier
Версия модели
Дата и время последнего сохранения модели
Имя пользователя, который последний раз сохранял модель
Опции анализа
В разделе «Опции анализа» приведены сведения о параметрах анализа Simulink Design Verifier.
В разделе «Опции анализа» перечислены параметры, которые повлияли на анализ Simulink Design Verifier. Если вы включили фильтр покрытия, имя файла фильтра будет включено в этот раздел.
Примечание
Для получения дополнительной информации об этих параметрах см. Раздел « Опции Simulink Design Verifier».
Неподдерживаемые блоки
Если ваша модель включает неподдерживаемые блоки, по умолчанию для продолжения анализа включено автоматическое упругость. При включенной автоматической закалке программное обеспечение рассматривает только интерфейс неподдерживаемых блоков, а не их фактическое поведение. Этот метод позволяет программному обеспечению завершить анализ. Однако анализ может достичь только частичных результатов, если любой из неподдерживаемых блоков модели повлияет на результат симуляции.
Раздел Неподдерживаемые блоки появляется только, если анализ упрямил неподдерживаемые блоки; в нем перечислены неподдерживаемые блоки в таблице с гиперссылкой на каждый блок модели.
Для получения дополнительной информации об автоматическом упрямстве см. Раздел «Несовместимость указателей с автоматическим упрямством».
Программные продукты
Раздел User Artifacts предоставляет информацию о тестовых данных и данных о покрытии в анализе Simulink Design Verifier.
Ограничения
В разделе «Ограничения» приведены сведения об условиях тестирования, которые Simulink Design Verifier применил при анализе модели.
Вы можете перейти к ограничению в модели, щелкнув гиперссылку в таблице Ограничения (Constraints). Программа подсвечивает соответствующий блок Test Condition в окне модели и открывает новое окно, показывающее блок подробно.
Сводные данные замен блоков
В Сводные данные Block Replacements представлен обзор замен блоков, выполненных Simulink Design Verifier. Оно появляется только в том случае, если Simulink Design Verifier заменил блоки в модели.
Каждая строка таблицы соответствует определенному правилу замены блоков, которое Simulink Design Verifier применил к модели. В таблице перечислены следующие элементы:
Имя файла, который содержит правило замены блоков и значение
BlockTypeпараметр, заданный правиломОписание правила, которое
MaskDescriptionпараметр блока замены задаетИмена блоков, которые Simulink Design Verifier заменил в модели
Чтобы найти конкретную замену блоков в модели, щелкните имя этой замены в столбце Замененные блоки таблицы; программа подсвечивает пострадавший блок в окне модели и открывает новое окно, которое подробно отображает блок.
Приближения
Каждая строка таблицы Приближений описывает определенный тип приближения, которую Simulink Design Verifier использовал во время анализа модели.
Примечание
Внимательно просмотрите результаты анализа, когда программное обеспечение использует приближения. В редких случаях приближение может привести к тестам, которые не достигают целей тестирования или контрпримеров, которые не фальсифицируют цели доказательства. Для примера ошибка округления с плавающей точкой может помешать сигналу превысить назначенное порогом значение.
Глава «Производные области значений»
В поиск ошибок проектирования анализе анализ вычисляет производные области значений значений сигналов для Outports для каждого блока в модели. Эта информация может помочь вам идентифицировать источник переполнения данных или ошибок деления на нули.
В таблице в Derived Ranges главе отчета об анализе перечислены эти границы.
Если блок Observer Reference используется в анализе поиска ошибок проектирования, то этот раздел покажет информацию о наблюдателе в Observer Model (s) подразделе и информацию о модели проекта в Design Model подразделе.
Таблица в Модель проекта подразделе показывает список всех производных областей значений в sldvdemo_debounce_validprop пример модели.
Раздел моделей (моделей ) (ов) наблюдателя не будет показывать производные области значений, о которых сообщается, поскольку наблюдатели игнорируются для поиска ошибок проектирования анализа.
Цели Главы состояния
В этом разделе отчета содержится информация обо всех целях в модели, включая тип цели, элемент модели, который соответствует типу, и описание цели.
Программа определяет наличие приближений и сообщает о них на уровне каждого объективного статуса. Для получения дополнительной информации смотрите Отчеты о приближениях через результаты валидации. В этой таблице обобщается целевой статус для режимов анализа Simulink Design Verifier.
| Режим анализа | Целевой статус |
|---|---|
|
Поиск ошибок проектирования |
|
|
Генерация тестов |
|
|
Проверка свойств |
|
Поиск ошибок проектирования состояния целей
Если вы запускаете анализ поиска ошибок проектирования, раздел Design Error Detection Objectives Status может включать следующие целевые статусы:
Если блок Observer Reference используется в анализе поиска ошибок проектирования, то этот раздел покажет информацию о наблюдателе в Observer Model(s) подразделе и информации о модели проекта в Design Model подразделе. Этот раздел будет пустым, если в модели нет активной логики.
Таблица в Модель проекта подразделе показывает список активной логики в sldvdemo_debounce_validprop пример модели.
Раздел моделей (моделей ) (ов) наблюдателя не покажет никакой активной логики, о которой сообщается, поскольку наблюдатели игнорируются для поиска ошибок проектирования анализа.
Мертвая логика. В 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 цели доказательства для модели 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 главу. В этой главе результирующие ошибки проектирования, которые анализ сфальсифицировал:
Таблица
Глава Ошибок проектирования содержит таблицу содержимого. Каждый элемент в таблицу содержимого является гиперссылкой на результаты относительно определенной ошибки проектирования.
Сводные данные
В Сводном разделе перечислены:
Элемент модели
Тип обнаруженной ошибки проектирования (переполнение или деление по нулю)
Статус анализа (сфальсифицированный или проверенный действительный)
В следующем примере программное обеспечение проанализировало sldvdemo_debounce_falseprop модель, чтобы обнаружить ошибки проектирования. Анализ обнаружил ошибку переполнения в блоке Sum в Подсистеме верификации с именем Verify True Output.
Тест
В разделе Тест перечислены временной шаг и соответствующее время, в течение которых тест фальсифицировал цель ошибки проектирования. Блок Inport raw имел значение 255, что вызвало ошибку переполнения.
Тесты»
При запуске анализа генерации тестов отчет включает главу Test Cases. Эта глава включает разделы, в которых обобщаются тесты, сгенерированные анализом:
Таблица
Глава Тестов содержит таблицу содержимого. Каждый элемент в таблицу содержимого является гиперссылкой на информацию о конкретном тесте.
Сводные данные
В Сводном разделе перечислены:
Длина сигналов, которые состоят из теста
Общее количество целей тестирования, которых достигает тест
Цели
В разделе «Цели» перечислены:
Временной шаг, на котором тест достигает этой цели.
Время, в которое тест достигает этой цели.
Ссылка на элемент модели, связанный с этой целью. При нажатии ссылки элемент модели подсвечивается в редакторе Simulink.
Цель, которая была достигнута с ссылкой перехода между главами Целей тестирования Status и Тестов.
Сгенерированные входные данные
Для каждого входного сигнала, связанного с элементом модели, раздел «Сгенерированные входные данные» приводит временной шаг и соответствующее время, в течение которых тест достигает конкретных целей тестирования. Если значение сигналов не изменяется в течение этих временных шагов, в таблице перечисляются временной шаг и время как области значений.
Примечание
Таблица Сгенерированные входные данные отображает штрих (-) вместо числа как значение сигналов, когда значение сигнала на том временном шаге не влияет на цель тестирования. В модели тестовой обвязки блок Inputs представляет эти значения с нулями, если вы не включите параметр Randomize data that does not affect outcome (см. «Рандомизируйте данные, которые не влияют на результат»).
Ожидаемый выход
Если вы выбираете Include expected output values на панели Design Verifier > Results диалогового окна Параметры конфигурации, отчет включает раздел Ожидаемый выход для каждого теста. Для каждого выходного сигнала, связанного с элементом модели, в этой таблице приводится ожидаемое выходное значение на каждом временном шаге.
Комбинированные цели
Если вы задаете для опции Test suite optimization значение CombinedObjectives (по умолчанию), глава «Случаи тестирования» может включать индивидуальную информацию о многих тестах.
Длинные тесты
Если вы задаете для опции Test suite optimization значение LongTestcasesГлава «Тесты» в отчете включает меньше разделов о более длинных тестах.
Свойства»
Если вы запускаете анализ проверки свойств, отчет включает в себя Properties главу. Эта глава включает разделы, в которых обобщаются цели доказательства и любые контрпримеры сгенерированного программного обеспечения:
Таблица
Глава Свойств содержит таблицу содержимого. Каждый элемент в таблицу содержимого является гиперссылкой на информацию об определенном свойстве, которое было сфальсифицировано.
Если блок Observer Reference используется в анализе доказательства свойств, то каждая глава свойств покажет информацию о наблюдателе в Observer Model(s) подразделе информацию о проектной модели в Design Model подразделе. Он будет пустым, когда в модели нет свойств.
Таблица показывает одно из свойств модели наблюдателя в sldvdemo_debounce_validprop пример модели.
Сводные данные
В Сводном разделе перечислены:
Элемент модели, который анализировало программное обеспечение
Тип свойства, которое было оценено
Состояние анализа
В следующем примере программное обеспечение проанализировало sldvdemo_cruise_control_verification модель для проверки свойств. Анализ доказал, что вход в Assertion блок с именем BrakeAssertion был ненулевым.
Контрпример
В разделе Counterexample перечислены временной шаг и соответствующее время, в которые контрпример сфальсифицировал свойство. В этом разделе также перечислены значения сигналов на том временном шаге.
