После анализа Simulink ® Design Verifier™ может создать HTML-отчет, содержащий подробную информацию о результатах анализа.
Отчет об анализе содержит гиперссылки, позволяющие:
Переход к определенной части отчета
Перейдите к объекту в модели Simulink, для которого анализ записал результаты.
Можно также создать дополнительную PDF-версию отчета Simulink Design Verifier.
Чтобы создать подробный отчет об анализе до или после анализа, выполните одно из следующих действий.
Перед анализом в диалоговом окне Параметры конфигурации (Configuration Parameters) на панели Проверка конструкции (Design Verifier) > Отчет (Report) выберите Создать отчет о результатах (Generate report of the results). Если требуется сохранить дополнительную PDF-версию отчета Simulink Design Verifier, выберите «Создать дополнительный отчет в формате PDF».
После анализа в окне журнала Simulink Design Verifier можно выбрать формат HTML или PDF и Создать подробный отчет об анализе.
Доклад начинается с двух разделов:
В разделе заголовка содержится следующая информация:
Проанализировано имя модели или подсистемы Simulink Design Verifier
Имя пользователя, связанное с текущим сеансом MATLAB ®
Дата и время создания отчета программой Simulink Design Verifier
Оглавление следует за разделом заголовка. Щелчок по элементам в оглавлении позволяет быстро перейти к отдельным главам отчета.
В главе Сводка отчета содержится следующая информация:
Имя модели
Выпуск MATLAB, в котором проводился анализ
Значение контрольной суммы, представляющее состояние анализируемой модели
Режим анализа
Представление модели
Цель генерации теста (применимо для анализа генерации теста)
Статус анализа
Время предварительной обработки
Время анализа
Состояние проанализированных целей. Это включает процентное число для каждого статуса.
Глава «Аналитическая информация» отчета включает следующие разделы:
В разделе Информация о модели (Model Information) представлены следующие сведения о текущей версии модели.
Путь и имя файла модели, проанализированные программой Simulink Design Verifier
Версия модели
Дата и время последнего сохранения модели
Имя пользователя, который в последний раз сохранял модель
В разделе «Параметры анализа» содержится информация о параметрах анализа Simulink Design Verifier.
В разделе Опции анализа (Analysis Options) перечислены параметры, повлиявшие на анализ Simulink Design Verifier. Если включена фильтрация покрытия, имя файла фильтра будет включено в этот раздел.
Примечание
Дополнительные сведения об этих параметрах см. в разделе Параметры Simulink Design Verifier.
Если модель включает неподдерживаемые блоки, по умолчанию включается автоматическое блокирование, позволяющее продолжить анализ. При включенном автоматическом блокировании программа учитывает только интерфейс неподдерживаемых блоков, а не их фактическое поведение. Этот метод позволяет программному обеспечению завершить анализ. Однако анализ может получить только частичные результаты, если какой-либо из неподдерживаемых блоков модели влияет на результат моделирования.
Раздел «Неподдерживаемые блоки» (Unsupported Blocks) появляется только в том случае, если анализ блокирует неподдерживаемые блоки; в нем перечислены неподдерживаемые блоки в таблице с гиперссылкой на каждый блок в модели.
Дополнительные сведения об автоматическом блокировании см. в разделе Обработка несовместимости с автоматическим блокированием.
В разделе «Артефакты пользователя» содержится информация о тестовых данных и данных покрытия в анализе Simulink Design Verifier.
В разделе Ограничения (Constraints) содержится информация о тестовых условиях, примененных Simulink Design Verifier при анализе модели.
Можно перейти к ограничению в модели, щелкнув гиперссылку в таблице Ограничения (Constraints). Программа подсвечивает соответствующий блок тестовых условий в окне модели и открывает новое окно с подробным отображением блока.
Сводка по заменам блоков содержит обзор замен блоков, выполненных программой Simulink Design Verifier. Она появляется, только если Simulink Design Verifier заменил блоки в модели.
Каждая строка таблицы соответствует определенному правилу замены блоков, которое Simulink Design Verifier применил к модели. В таблице перечислены следующие элементы:
Имя файла, содержащего правило замены блока и значение BlockType параметр, определяемый правилом
Описание правила, MaskDescription параметр блока замены указывает
Имена блоков, замененных программой Simulink Design Verifier в модели
Чтобы найти конкретную замену блока в модели, щелкните имя этой замены в столбце Замененные блоки (Replaced Blocks) таблицы; программа выделяет соответствующий блок в окне модели и открывает новое окно, в котором блок отображается подробно.
Каждая строка таблицы Аппроксимации описывает конкретный тип аппроксимации, который Simulink Design Verifier использовал при анализе модели.
Примечание
Внимательно просмотрите результаты анализа, если программа использует аппроксимации. В редких случаях аппроксимация может привести к тестовым случаям, которые не достигают целей тестирования, или контрпримерам, которые не могут фальсифицировать цели доказательства. Например, ошибка округления с плавающей запятой может предотвратить превышение сигналом заданного порогового значения.
При анализе обнаружения ошибок конструкции анализ вычисляет производные диапазоны значений сигналов для выходов для каждого блока в модели. Эта информация позволяет определить источник переполнения данных или ошибок деления на ноль.
Эти границы перечислены в таблице в главе «Производные диапазоны» отчета об анализе.
Если в анализе обнаружения ошибок конструкции используется ссылочный блок Observer, то в этом разделе будет показана информация о наблюдателе в подразделе Observer Model (s) и информация о конструкторской модели в подразделе Design Model.
Таблица в подразделе «Модель конструкции» показывает список каждого производного диапазона в sldvdemo_debounce_validprop пример модели.
В разделе Observer model (s) не будут отображаться производные диапазоны, так как наблюдатели игнорируются для анализа обнаружения ошибок конструкции.
В этом разделе отчета содержится информация обо всех целях модели, включая тип цели, элемент модели, соответствующий типу, и описание цели.
Программное обеспечение идентифицирует наличие аппроксимаций и сообщает о них на уровне каждого целевого статуса. Дополнительные сведения см. в разделе Отчеты о приближениях через результаты проверки. В этой таблице суммировано состояние цели для режимов анализа Simulink Design Verifier.
| Режим анализа | Статус цели |
|---|---|
|
Обнаружение ошибок конструкции | |
|
Генерация тестов | |
|
Проверка свойств |
При выполнении анализа обнаружения ошибок конструкции в разделе Состояние целей обнаружения ошибок конструкции могут быть указаны следующие целевые состояния.
Если в анализе обнаружения ошибок конструкции используется опорный блок Observer, то в этом разделе будут показаны сведения о наблюдателе в подразделе Observer Model (s) и сведения о конструкторской модели в подразделе Design Model. Этот раздел будет пустым, если в модели нет активной логики.
Таблица в подразделе Модель конструкции показывает список активных логик в sldvdemo_debounce_validprop пример модели.
В разделе Observer model (s) не будет отображаться какая-либо активная логика, так как наблюдатели игнорируются для анализа обнаружения ошибок конструкции.
Мертвая логика. В разделе Мертвая логика (Dead Logic) перечислены элементы, для которых анализ обнаружил мертвую логику.
На этом рисунке показан раздел Dead Logic созданного отчета об анализе для sldvdemo_fuelsys_logic_simple модель.
Мертвая логика (Dead Logic) в разделе Аппроксимация (Approximation). В разделе Мертвая логика (Dead Logic) в разделе Аппроксимация (Approximation) перечислены элементы модели, для которых анализ обнаружил мертвую логику при воздействии аппроксимации.
В версиях до R2017b этот раздел может включать цели, помеченные как Dead Logic.
На этом рисунке показана неработающая логика в разделе «Аппроксимация» созданного отчета об анализе.
Активная логика - требуется моделирование. В разделе Активная логика - требуется моделирование (Active Logic - Needs Simulation) перечислены элементы модели, для которых анализ обнаружил активную логику. Для подтверждения активного логического статуса необходимо выполнить дополнительное моделирование тестовых примеров.
В версиях до R2017b этот раздел может включать цели, помеченные как Active Logic.
На этом рисунке показана часть раздела «Активная логика - моделирование потребностей» созданного отчета об анализе для sldvdemo_fuelsys_logic_simple модель.
Цели действительны. В разделе Допустимые цели (Targets Valid) перечислены цели обнаружения ошибок конструкции, которые были признаны допустимыми при анализе. Для этих целей анализ определил, что описанные ошибки конструкции не могут произойти.
В версиях до R2017b этот раздел может включать цели, помеченные как проверенные как действительные.
На этом рисунке показан раздел «Действительные цели» созданного отчета об анализе для sldvdemo_design_error_detection модель.
Цели, действительные в разделе «Аппроксимация». В разделе Цели, допустимые для аппроксимации (Targets Valid in Approximation) перечислены цели обнаружения ошибок конструкции, которые анализ обнаружил действительными при воздействии аппроксимации.
В версиях до R2017b этот раздел может включать цели, помеченные как проверенные как действительные.
На этом рисунке показан раздел «Цели, действительные в аппроксимации» созданного отчета об анализе.
Сфальсифицированные цели - требуется моделирование. В разделе «Сфальсифицированные цели - моделирование потребностей» перечислены цели обнаружения ошибок конструкции, для которых в ходе анализа были обнаружены тестовые примеры, демонстрирующие ошибки конструкции. Для подтверждения фальсифицированного статуса необходимо выполнить дополнительное моделирование тестовых случаев.
В выпусках до R2017b этот раздел может включать цели, помеченные как Сфальсифицированные.
На этом рисунке показан раздел «Сфальсифицированные цели - моделирование потребностей» созданного отчета об анализе для sldvdemo_design_error_detection модель.
При выполнении анализа генерации тестового случая в раздел Статус целей тестирования могут быть включены следующие целевые статусы:
При анализе модели с целью покрытия модели, для которой установлено значение Enhanced MCDC, программное обеспечение сообщает о состоянии обнаружения элементов модели. Дополнительные сведения см. в разделе Расширенное покрытие MCDC в Simulink Design Verifier.
Если ссылочный блок Observer используется в анализе генерации тестового случая, то в каждом разделе статуса цели теста отображается информация о наблюдателе в подразделе Observer Model (s) информация о конструкторской модели в подразделе Design Model. Эти подразделы будут пустыми, если в модели не найдена цель теста .
В таблице показана часть целей, удовлетворяющих целям испытаний для режима проектирования в sldvdemo_debounce_testobjblks пример модели.
В таблице показана часть целей, удовлетворенных контрольными целями для модели наблюдателя в sldvdemo_debounce_testobjblks пример модели.
Цели выполнены. В разделе «Цели, удовлетворенные» перечислены цели тестирования, удовлетворяющие результатам анализа. Созданные тестовые примеры охватывают цели.
На этом рисунке показана часть раздела «Цели, удовлетворенные» созданного отчета об анализе для sldvdemo_fuelsys_logic_simple пример модели.
Цели выполнены - требуется моделирование. В разделе «Цели, удовлетворенные - требуется моделирование» перечислены цели тестирования, удовлетворяющие результатам анализа. Для подтверждения удовлетворенного статуса необходимо выполнить дополнительное моделирование тестовых случаев.
В выпусках до R2017b этот раздел может включать цели, отмеченные как Удовлетворенные.
На этом рисунке показан раздел «Цели, удовлетворенные - моделирование потребностей» созданного отчета об анализе.
Цели неудовлетворительны. В разделе «Цели неудовлетворительны» перечислены цели тестирования, которые не были выполнены при анализе.
В версиях до R2017b этот раздел может включать цели, отмеченные как проверенные как неудовлетворительные.
На этом рисунке показан раздел «Цели неудовлетворительны» созданного отчета об анализе для sldvdemo_fuelsys_logic_simple пример модели.
Цели неудовлетворительны в разделе «Приближение». В разделе «Цели, не удовлетворяемые» в разделе «Аппроксимация» перечислены цели испытаний, которые, как был определен анализ, не были удовлетворены из-за аппроксимации во время анализа.
В версиях до R2017b этот раздел может включать цели, отмеченные как проверенные как неудовлетворительные.
На этом рисунке показан раздел Цели, неудовлетворяемые в разделе Аппроксимация созданного отчета об анализе.
Цели не определены с помощью тестов. В разделе Цели, не определенные с помощью тестов, перечислены цели испытаний, которые не определены из-за влияния аппроксимации во время анализа.
В выпусках до R2017b этот раздел может включать цели, отмеченные как Удовлетворенные.
На этом рисунке показан раздел Цели, не определенные с помощью тестов, созданного отчета об анализе для sldvApproximationsExample пример модели.
При выполнении анализа, подтверждающего свойства, раздел «Состояние целей подтверждения» может включать в себя следующее:
Если в анализе, подтверждающем свойства, используется ссылочный блок Observer, то в каждом разделе статуса объективной проверки будет отображаться информация о наблюдателе в подразделе Observer Model (s) и информация о конструкторской модели в подразделе Design Model. Эти подразделы будут пустыми, если в модели не будет найдена цель.
В таблице показаны цели Действительные цели подтверждения для модели Observer в sldvdemo_debounce_validprop пример модели.
Цели действительны. В разделе «Действительные цели» перечислены подтверждающие цели, которые анализ обнаружил действительными.
В версиях до R2017b этот раздел может включать цели, помеченные как проверенные как действительные.
На этом рисунке показан раздел «Действительные цели» созданного отчета об анализе для sldvdemo_debounce_validprop пример модели.
Цели, действительные в разделе «Аппроксимация». В разделе Цели, действительные для аппроксимации перечислены цели подтверждения, которые анализ нашел действительными при воздействии аппроксимации.
В версиях до R2017b этот раздел может включать цели, помеченные как цели, проверенные как действительные.
На этом рисунке показан раздел «Цели, действительные в аппроксимации» созданного отчета об анализе.
Цели, сфальсифицированные контрпримерами. В разделе «Цели, сфальсифицированные контрпримерами» перечислены цели доказательства, которые были опровергнуты в ходе анализа. Созданный контрпример показывает нарушение цели доказательства.
На этом рисунке показан раздел «Цели, сфальсифицированные контрпримерами» созданного отчета об анализе для sldvdemo_debounce_falseprop пример модели.
Сфальсифицированные цели - требуется моделирование. В разделе «Сфальсифицированные цели - моделирование потребностей» перечислены цели проверки, которые были опровергнуты при анализе. Для подтверждения фальсифицированного статуса необходимо выполнить дополнительное моделирование контрпримеров.
В выпусках до R2017b этот раздел может включать цели, помеченные как Цели, сфальсифицированные контрпримерами.
На этом рисунке показан раздел «Сфальсифицированные цели - моделирование потребностей» созданного отчета об анализе.
Цели не определены с помощью контрпримеров. В разделе «Цели, не определенные с помощью контрпримеров» перечисляются цели доказательства, не определенные из-за влияния аппроксимации во время анализа.
В выпусках до R2017b этот раздел может включать цели, помеченные как Сфальсифицированные.
На этом рисунке показан раздел «Цели, не определенные с помощью контрпримеров» созданного отчета об анализе.
Для целей проверки и целей тестирования в разделе Цели, не определенные из-за ошибки во время выполнения, перечислены неопределившиеся цели во время анализа из-за ошибки во время выполнения. Ошибка во время выполнения во время моделирования тестового случая или контрпримера.
В выпусках до R2017b этот раздел может включать цели, помеченные как Сфальсифицированные или Удовлетворенные.
На этом рисунке показан раздел «Цели не определены из-за ошибки во время выполнения» созданного отчета об анализе.
Для всех типов целей в разделе Цели, не определенные из-за деления на ноль перечислены неопределившиеся цели во время анализа из-за ошибок разделения на ноль в связанных элементах модели. Чтобы обнаружить ошибки деления на ноль перед выполнением дальнейшего анализа модели, выполните процедуру, описанную в разделе Обнаружение переполнения целых чисел и Ошибки деления на ноль.
Для всех типов целей в разделе Цели, не определенные из-за нелинейности перечисляются неопределившиеся цели во время анализа из-за требуемого вычисления нелинейной арифметики. Simulink Design Verifier не поддерживает нелинейную арифметическую или нелинейную логику.
Для всех типов целей в разделе Цели, не определенные из-за тупика перечисляются элементы модели с неопределившимися целями во время анализа из-за тупика. В выпусках, предшествующих R2013b, эти цели могут включать цели, помеченные как Цели, удовлетворенные - Нет тестового случая или Цели сфальсифицированы - Нет Контрпримера.
Для всех типов целей в разделе Цели, не определенные из-за массива вне границ (Targets Undecided Due to Array Out of Bounds) перечислены неопределившиеся цели во время анализа из-за ошибок массива вне границ в связанных элементах модели. Чтобы обнаружить ошибки массива вне границ в модели, см. раздел Обнаружение ошибок доступа к массиву вне границ.
Для всех типов целей в разделе «Цели не определены» перечислены цели, для которых анализ не смог определить результат за отведенное время.
В этом примере проверки свойств программное обеспечение превысило предельное время анализа (указанное параметром Maximum analysis time) или было прервано до завершения обработки этих целей.
В главе «Элементы модели» отчета содержится таблица для каждого объекта модели, определяющая цели покрытия. В таблице для конкретного объекта перечислены все связанные цели, типы целей, описания целей и статус каждой цели в конце анализа.
Таблица для отдельного объекта в модели выглядит аналогично этой таблице для интегратора дискретного времени в подсистеме PI Controller sldvdemo_cruise_control пример модели.
Чтобы выделить данный объект в модели, щелкните Вид (View) в левом верхнем углу таблицы; программа открывает новое окно, в котором объект отображается подробно. Чтобы просмотреть сведения о тестовом случае, примененном к определенной цели, щелкните номер тестового случая в последнем столбце таблицы.
Если в анализе проверки свойств используется ссылочный блок Observer, то в каждом разделе элемента модели отображается информация о наблюдателе в подразделе Observer Model (s) информация о конструкторской модели в подразделе Design Model. Эти подразделы будут пустыми, если в модели не найдена цель теста.
В таблице показана одна из целей испытаний для конструкторской модели в sldvdemo_debounce_testobjblks пример модели.
В таблице показана одна из целей теста для модели наблюдателя в sldvdemo_debounce_testobjblks пример модели.
Если выполняется анализ обнаружения ошибок конструкции, а анализ обнаруживает ошибки конструкции в модели, в отчет включена глава Ошибки конструкции (Design Errors). В этой главе обобщаются ошибки проектирования, которые были сфальсифицированы при анализе:
В главе «Ошибки проектирования» содержится оглавление. Каждый элемент в оглавлении является гиперссылкой на результаты о конкретной ошибке конструкции.
В разделе Сводка перечислены:
Элемент модели
Тип обнаруженной ошибки конструкции (переполнение или деление на ноль)
Статус анализа (фальсифицированный или подтвержденный)
В следующем примере программное обеспечение проанализировало sldvdemo_debounce_falseprop модель для обнаружения ошибок конструкции. Анализ обнаружил ошибку переполнения в блоке Sum в подсистеме проверки с именем Verify True Output.
В разделе «Тестовый случай» перечислены временной шаг и соответствующее время, в которое тестовый случай сфальсифицировал цель ошибки конструкции. Блок ввода raw имел значение 255, что вызвало ошибку переполнения.
При выполнении анализа генерации теста в отчет включена глава «Тестовые примеры». В этой главе содержатся разделы, в которых обобщаются созданные результаты анализа:
В главе Test Cases содержится содержание. Каждый элемент в оглавлении представляет собой гиперссылку на информацию о конкретном тестовом случае.
В разделе Сводка перечислены:
Длина сигналов, составляющих тестовый случай
Общее количество целей теста, достигаемых в тестовом случае
В разделе Цели перечислены:
Временной шаг, на котором тест достигает этой цели.
Время, в которое тест достигает этой цели.
Ссылка на элемент модели, связанный с этой целью. Щелчок по ссылке подсвечивает элемент модели в редакторе Simulink.
Цель, которая была достигнута с помощью ссылки для перехода между главами «Состояние целей тестирования» и «Примеры тестирования».
Для каждого входного сигнала, связанного с элементом модели, в разделе Сгенерированные входные данные (Generated Input Data) перечислены временной шаг и соответствующее время, в которое тестовый случай достигает конкретных целей теста. Если значение сигнала не изменяется в течение этих временных шагов, в таблице в качестве диапазонов указаны временной шаг и время.
Примечание
Таблица Сгенерированные входные данные (Generated Input Data) отображает тире (-) вместо числа в качестве значения сигнала, когда значение сигнала на этом шаге времени не влияет на цель теста. В модели кабельных трасс блок Входы (Inputs) представляет эти значения с нулями, если не включить параметр Рандомизировать (Randomize), не влияющий на параметр результата (см. раздел Рандомизация данных, не влияющих на результат).
Если на панели Design Verifier (Проверка проекта) > Results (Результаты) диалогового окна Configuration Parameters (Параметры конфигурации) выбрать Include expected output values (Включить ожидаемые выходные значения), в отчет будет включен раздел Expected Output (Ожидаемые выходные данные) для каждого тестового случая. Для каждого выходного сигнала, связанного с элементом модели, в этой таблице отображается ожидаемое выходное значение на каждом временном шаге.
Если для параметра Оптимизация набора тестов установлено значение CombinedObjectives (по умолчанию), глава Test Cases может содержать индивидуальную информацию о многих тестовых случаях.
Если для параметра Оптимизация набора тестов установлено значение LongTestcases, глава Test Cases в отчете содержит меньше разделов о более длинных тестовых случаях.
При выполнении анализа, подтверждающего свойства, отчет содержит главу «Свойства». Эта глава содержит разделы, в которых обобщаются цели проверки и любые контрпримеры, касающиеся созданного программного обеспечения:
В главе «Свойства» содержится оглавление. Каждый элемент в оглавлении является гиперссылкой на сведения о конкретном свойстве, которое было сфальсифицировано.
Если в анализе проверки свойств используется ссылочный блок Observer, то каждая глава свойств покажет информацию о наблюдателе в подразделе Observer Model (s) информацию о конструкторской модели в подразделе Design Model. Он будет пустым, если в модели нет свойств.
В таблице показано одно из свойств модели наблюдателя в sldvdemo_debounce_validprop пример модели.
В разделе Сводка перечислены:
Элемент модели, проанализированный программным обеспечением
Тип вычисляемого свойства
Статус анализа
В следующем примере программное обеспечение проанализировало sldvdemo_cruise_control_verification модель для проверки свойств. Анализ доказал, что вход в блок Assertion с именем IntegrationAssertion был ненулевым.
В разделе «Контрпример» перечислены временной шаг и соответствующее время, в которое контрпример сфальсифицировал свойство. В этом разделе также перечислены значения сигналов на этом временном шаге.
