Следующие разделы описывают модель 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, чтобы получить выходной сигнал
Соедините эти блоки такой, таким образом, ваша модель кажется похожей на следующую модель:
На вкладке Modeling нажмите Model Settings.
На диалоговом окне Configuration Parameters, в панели 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 модель.
На вкладке Design Verifier нажмите Check Compatibility.
Программное обеспечение 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 модель.
На вкладке Design Verifier, в разделе Mode, выбирают Property Proving.
Нажмите Property Proving Settings.
Нажмите OK, чтобы применить ваши изменения и закрыть диалоговое окно Configuration Parameters.
Примечание
На панели Property Proving можно опционально задать значения для других параметров, которые управляют, как Simulink Design Verifier доказывает свойства модели. Для получения дополнительной информации смотрите Панель Верификатора Проекта: Доказательство Свойства.
Сохраните ex_property_proving_example_basic модель.
Анализировать ex_property_proving_example_basic модель, на вкладке Design Verifier, нажимает Prove Properties. Simulink Design Verifier начинает доказывающий свойство анализ.
Во время анализа логарифмическое окно показывает прогресс анализа. Это отображает информацию, такую как количество обработанных целей и каким целям удовлетворили или сфальсифицировали.
Чтобы отключить анализ в любое время, в логарифмическом окне, нажимают Stop.
Когда анализ завершен, логарифмическое окно отображает следующие опции для рассмотрения результатов:
Подсветите результаты анализа на модели
Сгенерируйте подробный аналитический отчет HTML
Создайте модель тестовой обвязки с тестами
Симулируйте тесты, созданные моделью, и представьте отчет покрытия модели
Можно также просмотреть файл данных Simulink Design Verifier. Для получения дальнейшей информации о файле данных, смотрите Файлы данных Simulink Design Verifier.
Следующие разделы описывают, как можно рассмотреть результаты анализа:
Можно рассмотреть результаты анализа сразу путем просмотра блоков, которые подсвечены в окне модели. Выделение может иметь четыре цвета:
Зеленый — анализ доказал все допустимые цели доказательства.
Красный — анализ опроверг цель доказательства и сгенерировал контрпример, который сфальсифицировал ту цель.
Оранжевый — анализ опроверг цель доказательства, но он не мог сгенерировать контрпример, или цель доказательства осталась нерешенной. Этот результат происходит из-за:
Цель доказательства на сигнале, значение которого программное обеспечение не может управлять, например, блоком Constant
Цель доказательства, которая зависит от нелинейного расчета
Цель доказательства, которая создает арифметическую ошибку, такую как деление на нуль
Автоматическое блокирование, включаемое, и анализ, сталкивающийся с неподдерживаемым блоком, операцию которого это не изучает, но что анализ требует, чтобы сгенерировать контрпример
Аналитический таймаут
Ограничения аналитического механизма
Серый — объект модели не был частью анализа.
Подсветите результаты анализа на модели в качестве примера:
В окне Results Summary для ex_property_proving_example_basic анализ, нажмите Highlight analysis results on model.
Блок Proof Objective подсвечен в красном, который указывает, что цель доказательства была сфальсифицирована с контрпримером.
Окно Simulink Design Verifier Results появляется.
Когда вы кликаете по объектам в модели, это окно изменяется, чтобы отобразить результаты детального анализа для того объекта.
Совет
По умолчанию окно Simulink Design Verifier Results всегда является самым верхним видимым окном. Чтобы позволить окну перемещаться позади другого окна, кликните
и очистите Always on top.
Кликните по подсвеченному блоку Proof Objective.
Окно Simulink Design Verifier Results указывает, что цель доказательства, что выходной сигнал от Сравнивания до Нуля не был 1, была опровергнута с контрпримером.
Создать подробный аналитический отчет HTML:
В окне Simulink Design Verifier Results Summary нажмите 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 модель.
На вкладке Simulation нажмите 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 в окне Results Summary.
На вкладке Design Verifier, в разделе Review Results, нажимают Results Summary. Окно Results Summary открывает отображение результатов последнего анализа Simulink Design Verifier.
Для любого анализа Simulink Design Verifier, из окна Results Summary, можно выполнить следующие задачи.
| Задача | Для получения дополнительной информации |
|---|---|
Подсветите результаты анализа на модели. | Подсвеченные результаты на модели |
Сгенерируйте отчет детального анализа. | Отчеты 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 модель. На вкладке Design Verifier нажмите Prove Properties.
Когда анализ завершен, логарифмическое окно отображает опции. Нет никакой опции, чтобы создать модель тестовой обвязки, потому что анализ удовлетворил всем целям доказательства в вашей модели, таким образом, нет никаких контрпримеров.
Рассмотрите результаты второго анализа:
Подсветите модель, чтобы видеть результаты анализа:
Нажмите 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, программное обеспечение обнаружило противоречие в вашей модели, и это не может анализировать модель. У вас может быть противоречие, если ваша модель имеет блоки Proof Assumption неправильными параметрами. Например, предположение могло утвердить, что сигнал должен быть между 0 и 5, когда сигнал постоянный 10.
Если программное обеспечение обнаруживает противоречие, все предыдущие результаты делаются недействительным, и программное обеспечение сообщает, что все свойства сфальсифицированы.
Примечание
Ограничения, добавленные во входных параметрах или через минимум/максимум проекта или через тестовые предположения условий/доказательства, не приводят к противоречию. Однако, если вы ограничиваете сигналы, которые являются нисходящими из расчета с помощью тестовых предположений условий/доказательства, необходимо гарантировать, что ограниченное условие выполнимо посредством расчета модели. В противном случае получившаяся модель является противоречащей, который может приводить к недопустимым результатам с или без явной аналитической ошибки. Чтобы гарантировать, что ограничения выполнимы, сначала попробуйте то же условие с помощью Цели тестирования. Если этому можно удовлетворить, можно использовать то же условие безопасно в качестве ограничения.
Полное доказательство вашей модели требует, чтобы Simulink Design Verifier перерыл все достижимые настройки вашей модели — даже те, которые достигнуты только после долговременных задержек. Время вычисления и память, требуемая искать модель полностью часто, делают исчерпывающее доказательство непрактичным.
Prove Properties в Больших моделях дает подробную информацию о стратегиях, которые можно использовать, чтобы улучшать производительность доказывающего свойство анализа большой модели.
