Следующие разделы описывают модель Simulink®, для которой вы доказываете свойство, что вы задаете использование блока Proof Objective. Этот пример демонстрирует доказывающие свойство возможности Simulink Design Verifier™.
В этом примере вы выполняете следующие задачи.
| Задача | Описание | Смотрите... |
|---|---|---|
| 1 | Создайте модель в качестве примера. | |
| 2 | Проверьте, что ваша модель совместима с Simulink Design Verifier. | |
| 3 | Добавьте блок Proof Objective в свою модель, чтобы подготовиться к ее доказательству. | |
| 4 | Сконфигурируйте Simulink Design Verifier, чтобы доказать свойства. | |
| 5 | Докажите свойство своей модели. | |
| 6 | Рассмотрите результаты анализа. | |
| 7 | Добавьте предположения доказательства, чтобы задать аналитические ограничения. | |
| 8 | Докажите свойство индивидуально настраиваемой модели и интерпретируйте результаты. |
Создайте модель Simulink, чтобы использовать в этом примере:
Создайте пустую модель Simulink.
Скопируйте следующие блоки в свое пустое окно модели:
От библиотеки Sources, блок Inport, чтобы инициировать входной сигнал, чье значение средства управления Simulink Design Verifier
От библиотеки Logic и Bit Operations, блок Compare To Zero, чтобы обеспечить простую логику
От библиотеки Sinks, блок Outport, чтобы получить выходной сигнал
Соедините эти блоки такой, таким образом, ваша модель кажется подобной следующей модели:
В окне модели выберите Simulation> Model Configuration Parameters.
На левой стороне диалогового окна Configuration Parameters, в дереве Select, кликают по категории Solver. На правой стороне, под Solver selection:
Установите опцию Type на Fixed-step.
Установите опцию Solver на Discrete (no continuous states).
Simulink Design Verifier может анализировать только модели, которые используют решатель фиксированного шага.
Нажмите OK, чтобы сохранить ваши изменения и закрыть диалоговое окно Configuration Parameters.
Сохраните свою модель с именем ex_property_proving_example_basic.
Каждый раз программное обеспечение Simulink Design Verifier анализирует модель, прежде чем анализ начнется, программное обеспечение выполняет проверку совместимости. Если ваша модель не совместима, программное обеспечение не может анализировать ее.
Можно также убедиться вы, модель совместима с Simulink Design Verifier, прежде чем вы запустите анализ:
Откройте модель ex_property_proving_example_basic.
В окне модели выберите Analysis> Design Verifier> Check Compatibility> Model.
Программное обеспечение Simulink Design Verifier отображает логарифмическое окно, которое утверждает, совместима ли ваша модель.
Модель, которую вы только создали, совместима.
Если проверка совместимости указывает, что ваша модель частично совместима, ваша модель содержит по крайней мере один объект, который не поддерживает Simulink Design Verifier. Можно анализировать частично совместимую модель, но по умолчанию неподдерживаемые объекты погашены. Результаты анализа могут быть неполными. Для получения дальнейшей информации об автоматическом блокировании, смотрите Несовместимости Указателя с Автоматическим Блокированием.
Подготовьте свою модель в качестве примера так, чтобы можно было доказать ее свойства с Simulink Design Verifier. А именно, оснастите модель путем добавления и конфигурирования блока Proof Objective:
В Командном окне MATLAB® введите sldvlib.
Библиотека Simulink Design Verifier появляется.
Откройте подбиблиотеку Objectives и Constraints.
Скопируйте блок Proof Objective в свою модель и вставьте его между Сравниванием С блоками Нуля и Выходного порта.
В вашей модели дважды кликните блок Proof Objective.
Диалоговое окно параметров блоков Цели доказательства открывается.
В поле Values введите 1.
Программное обеспечение Simulink Design Verifier попытается доказать, что сигнал, выведенный блоком Compare To Zero всегда, достигает этого значения для любых сигналов, что это получает.
Нажмите OK, чтобы применить ваши изменения и закрыть диалоговое окно параметров блоков Цели доказательства.
Сохраните свою модель и сохраните ее открытой.
Сконфигурируйте Simulink Design Verifier, чтобы доказать свойства модели ex_property_proving_example_basic, которую вы оснастили:
Откройте модель ex_property_proving_example_basic.
В вашем окне модели Simulink выберите Analysis> Design Verifier> Options.
На левой стороне диалогового окна Configuration Parameters, в дереве Select, выбирают категорию Design Verifier. Под Analysis options на правой стороне, установленной параметр Mode на Property proving.
Нажмите OK, чтобы применить ваши изменения и закрыть диалоговое окно Configuration Parameters.
На панели Property Proving можно опционально задать значения для других параметров, которые управляют, как Simulink Design Verifier доказывает свойства модели. Для получения дополнительной информации смотрите Панель Верификатора Проекта: Доказательство Свойства.
Сохраните модель ex_property_proving_example_basic.
Чтобы анализировать модель ex_property_proving_example_basic, в окне модели, выбирают Analysis> Design Verifier> Prove Properties> Model. Программное обеспечение Simulink Design Verifier начинает доказывающий свойство анализ.
Во время анализа логарифмическое окно показывает прогресс анализа. Это отображает информацию, такую как количество обработанных целей и какие цели были удовлетворены или сфальсифицированы.
Чтобы отключить анализ в любое время, в логарифмическом окне, нажимают Stop.
Когда анализ завершен, логарифмическое окно отображает следующие опции для рассмотрения результатов:
Подсветите результаты анализа на модели
Сгенерируйте подробный аналитический отчет HTML
Создайте модель тестовой обвязки с тестами
Моделируйте тесты, созданные моделью, и представьте отчет покрытия модели
Можно также просмотреть файл данных Simulink Design Verifier. Для получения дальнейшей информации о файле данных, смотрите Файлы данных Simulink Design Verifier.
Следующие разделы описывают, как можно рассмотреть результаты анализа:
Можно рассмотреть результаты анализа сразу путем просмотра блоков, которые подсвечены в окне модели. Выделение может иметь четыре цвета:
Зеленый — анализ доказал все допустимые цели доказательства.
Красный — анализ опроверг цель доказательства и сгенерировал контрпример, который сфальсифицировал ту цель.
Оранжевый — анализ опроверг цель доказательства, но он не мог сгенерировать контрпример, или цель доказательства осталась нерешенной. Этот результат происходит из-за:
Цель доказательства на сигнале, значение которого программное обеспечение не может управлять, например, блоком Constant
Цель доказательства, которая зависит от нелинейного вычисления
Цель доказательства, которая создает арифметическую ошибку, такую как деление на нуль
Автоматическое блокирование, включаемое, и анализ, сталкивающийся с неподдерживаемым блоком, операцию которого это не понимает, но что анализ требует, чтобы сгенерировать контрпример
Аналитический таймаут
Ограничения аналитического механизма
Серый — объект модели не был частью анализа.
Подсветите результаты анализа на модели в качестве примера:
В логарифмическом окне для анализа ex_property_proving_example_basic нажмите Highlight analysis results on model.
Блок Proof Objective подсвечен в красном, который указывает, что цель доказательства была сфальсифицирована с контрпримером.
Окно Simulink Design Verifier Results появляется.
Когда вы кликаете по объектам в модели, это окно изменяется на результаты детального анализа отображения для того объекта.
По умолчанию окно Simulink Design Verifier Results всегда является самым верхним видимым окном. Чтобы позволить окну перемещаться позади другого окна, щелкните
и очиститесь Поверх остальных окон.
Кликните по подсвеченному блоку Proof Objective.
Окно Simulink Design Verifier Results указывает, что цель доказательства, что выходной сигнал от Сравнивания до Нуля не был 1, была опровергнута с контрпримером.
Создать подробный аналитический отчет HTML:
В логарифмическом окне Simulink Design Verifier нажмите Generate detailed analysis report.
Отчет HTML открывается в окне браузера.
Отчет включает в себя следующий Table of Contents. Кликните по гиперссылке, чтобы перейти к конкретному разделу в отчете.
В Table of Contents нажмите Summary.
Сводные данные предоставляют обзор результатов анализа, и они указывают, что Simulink Design Verifier идентифицировал контрпример, который фальсифицирует цель в вашей модели.
Прокрутите назад к верхней части окна браузера. В Table of Contents нажмите Proof Objectives Status.
Таблица Objectives Falsified with Counterexamples приводит цели доказательства, что Simulink Design Verifier опроверг использование контрпримера, который это сгенерировало. Можно определить местоположение цели в окне модели путем нажатия на Proof Objective; программное обеспечение подсвечивает соответствующий блок Proof Objective в вашем окне модели.
В таблице Objectives Falsified with Counterexamples, в соответствии со столбцом Counterexample, нажимают 1.
Этот раздел отображает информацию о цели доказательства 1 и предоставляет подробную информацию о контрпримере, который Simulink Design Verifier сгенерировал, чтобы опровергнуть ту цель. В этом контрпримере значение сигналов 99 фальсифицирует цель, что вы задали использование блока Proof Objective. Таким образом, 99 не меньше чем или равно 0, который заставляет блок Compare To Zero возвращать 0 (FALSE) вместо 1 (TRUE).
Создайте модель тестовой обвязки с контрпримерами, которые фальсифицируют цели доказательства в вашей модели:
В логарифмическом окне Simulink Design Verifier нажмите Create harness model.
Программное обеспечение создает модель тестовой обвязки под названием ex_property_proving_example_basic_harness.
Модель тестовой обвязки содержит следующие элементы:
Блок Signal Builder под названием Inputs — группа сигналов, которые фальсифицируют цели доказательства.
Блок Subsystem под названием Test Unit — копия вашей модели.
DocBlock по имени Test Case Explanation — текстовое описание контрпримеров, которые генерирует анализ.
Блок Size-Type — подсистема, которая передает сигналы от блока Inputs до блока Test Unit. Этот блок проверяет, что размер и тип данных сигналов сопоставимы с блоком Test Unit.
Дважды кликните блок Inputs.
Входной сигнал 1 причина вывод блока Compare to Zero, чтобы быть 0. Этот контрпример нарушает цель доказательства, которая указывает, что вывод блока Compare to Zero 1.
Моделируйте модель тестовой обвязки, чтобы наблюдать контрпример, который фальсифицирует цель доказательства в вашей модели:
В окне модели ex_property_proving_example_basic выберите View> Library Browser
От библиотеки Sinks скопируйте блок Scope в свое окно модели тестовой обвязки. Блок Scope позволяет вам видеть значение сигнала, выведенного блоком Compare To Zero в вашей модели.
В вашем окне модели тестовой обвязки соедините выходной сигнал Тестовой Модульной подсистемы к блоку Scope.
В вашем окне модели тестовой обвязки выберите Simulation> Run, чтобы начать симуляцию.
Программное обеспечение Simulink моделирует модель тестовой обвязки.
В вашем окне модели тестовой обвязки дважды кликните блок Scope, чтобы открыть его окно экрана.
Блок Scope отображает значение сигнала, выведенного блоком Compare To Zero в вашей модели. В этом примере блок Compare To Zero возвращает 0 (FALSE) в течение симуляции, которая фальсифицирует цель доказательства что вывод блока Compare to Zero быть 1 (TRUE). Контрпример, что предоставления блока Signal Builder фальсифицируют цель доказательства.
Пока ваша модель остается открытой, можно просмотреть результаты новых результатов анализа Simulink Design Verifier в Model Explorer.
В Редакторе Simulink выберите Analysis> Design Verifier > Latest Results. Model Explorer открывается, и результаты последнего анализа Simulink Design Verifier появляются в правой панели.
Для любого анализа Simulink Design Verifier, от Model Explorer, можно выполнить следующие задачи.
| Задача | Для получения дополнительной информации |
|---|---|
Подсветите результаты анализа на модели. | Подсвеченные результаты на модели |
Сгенерируйте отчет детального анализа. | Отчеты Simulink Design Verifier |
Создайте модель тестовой обвязки, или если модель тестовой обвязки уже существует, откройте его. Если никакие контрпримеры не были созданы во время анализа, эта опция не доступна. | Модели тестовой обвязки Simulink Design Verifier |
Просмотрите файл данных. | Файлы данных Simulink Design Verifier |
Просмотрите файл журнала. | Файлы журнала Simulink Design Verifier |
После того, как вы закроете свою модель, вы больше не можете просматривать результаты анализа.
Измените простую модель Simulink, цель доказательства которой Simulink Design Verifier опроверг в предыдущей задаче. А именно, настройте доказательство путем добавления и конфигурирования блока Proof Assumption:
В Окне Команды MATLAB введите sldvlib.
Библиотека Simulink Design Verifier открывается.
Откройте подбиблиотеку Objectives и Constraints.
Скопируйте блок Proof Assumption в свою модель.
В вашем окне модели вставьте блок Proof Assumption между Inport и Compare, Чтобы Обнулить блоки.
В вашей модели дважды кликните блок Proof Assumption, чтобы получить доступ к его атрибутам.
Диалоговое окно параметров блоков Предположения Доказательства открывается.
В поле Values введите [-1, 0]. При доказательстве свойств этой модели Simulink Design Verifier ограничивает значения сигналов, вводящие блок Compare To Zero в заданную область значений. Если вход к блоку Compare to Zero всегда будет в этой области значений, вывод блока Compare to Zero всегда будет 1.
Нажмите Apply и затем OK, чтобы применить ваши изменения и закрыть диалоговое окно параметров блоков Предположения Доказательства.
Сохраните модель ex_property_proving_example_basic и сохраните ее открытой.
Анализируйте модель, которую вы изменили, чтобы видеть, как блок Proof Assumption влияет на доказывающий свойство анализ.
В окне модели ex_property_proving_example_basic выберите Analysis> Design Verifier> Prove Properties> Model.
Когда анализ завершен, логарифмическое окно отображает опции. Нет никакой опции, чтобы создать модель тестовой обвязки, потому что анализ удовлетворил все цели доказательства в вашей модели, таким образом, нет никаких контрпримеров.
Рассмотрите результаты второго анализа:
Подсветите модель, чтобы видеть результаты анализа:
Нажмите Highlight analysis results on model.
Цель доказательства теперь подсвечена в зеленом.
Кликните по блоку Proof Objective.
Окно Simulink Design Verifier Results показывает, что цель доказательства, которая утверждает, что сигнал быть 1 допустим.
Рассмотрите результаты анализа в подробном отчете:
Нажмите Generate detailed analysis report.
В Table of Contents нажмите Summary.
Итоговая глава указывает, что Simulink Design Verifier доказал цель доказательства в модели.
Раздел Constraints перечисляет аналитическое ограничение, которое вы задали в блоке Proof Assumption.
Прокрутите назад к верхней части окна браузера. В Table of Contents нажмите Proof Objectives Status.
Таблица Objectives Proven Valid приводит цели доказательства, что Simulink Design Verifier оказался допустимым.
Прокрутите вниз, чтобы просмотреть главу Свойств или перейти к верхней части окна браузера и в Table of Contents, нажать Properties.
Сводные данные Цели доказательства указывают, что Simulink Design Verifier доказал цель, которую вы задали в своей модели. Блок Proof Assumption ограничивает область входных сигналов к интервалу [-1, 0]. Поэтому программное обеспечение доказывает, что этот интервал не содержит значения, которые больше, чем нуль, таким образом, удовлетворяя цель доказательства.
Если анализ производит ошибку The model is contradictory in its current configuration, программное обеспечение обнаружило противоречие в вашей модели, и это не может анализировать модель. У вас может быть противоречие, если ваша модель имеет блоки Предположения Доказательства с неправильными параметрами. Например, предположение могло утвердить, что сигнал должен быть между 0 и 5, когда сигнал постоянный 10.
Если программное обеспечение обнаруживает противоречие, все предыдущие результаты делаются недействительным, и программное обеспечение сообщает, что все свойства сфальсифицированы.
Полное доказательство вашей модели требует, чтобы Simulink Design Verifier перерыл все достижимые настройки вашей модели — даже те, которые достигнуты только после долговременных задержек. Время вычисления и память, требуемая искать модель полностью часто, делают исчерпывающее доказательство непрактичным.
Prove Properties в Больших моделях дает подробную информацию о стратегиях, которые можно использовать, чтобы улучшать производительность доказывающего свойство анализа большой модели.
