Доказательство свойств в модели
Об этом примере
В следующих разделах описывается Simulink® модель, для которой вы доказываете свойство, которое вы задаете используя блок Цель Доказательства. Этот пример демонстрирует возможности проверки свойств Simulink Design Verifier™.
В этом примере вы выполняете следующие задачи.
| Задача | Описание | Видите... |
|---|---|---|
| 1 | Создайте модель примера. | |
| 2 | Проверьте, что ваша модель совместима с Simulink Design Verifier. | |
| 3 | Добавьте цель доказательства к модели, чтобы подготовиться к его доказательству. | |
| 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.
В диалоговом окне Параметров конфигурации, в панели Solver, в Solver selection:
Установите значение опции Type
Fixed-step.Установите значение опции Solver
Discrete (no continuous states).
Simulink Design Verifier может анализировать только модели, которые используют решатель с фиксированным шагом.
Нажмите кнопку OK, чтобы сохранить изменения и закрыть диалоговое окно Параметры конфигурации.
Сохраните модель с именем
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.
Откройте вложенный раздел Цели и ограничения.
Скопируйте блок Цель Доказательства в модель и вставьте его между блоками Compare To Zero и Outport.
В модели дважды кликните блок Цель Доказательства.
Откроется диалоговое окно Цели доказательства параметров блоков.
В 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, чтобы применить изменения и закрыть диалоговое окно Параметры конфигурации.
Примечание
На панели Property Proving можно опционально задать значения для других параметров, которые управляют тем, как Simulink Design Verifier доказывает свойства вашей модели. Дополнительные сведения см. в разделе Панель Design Verifier: Property Proving.
Сохраните
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.
В следующих разделах описывается, как можно просмотреть результаты анализа:
Просмотр результатов по модели
Можно просмотреть результаты анализа с первого взгляда, просматривая блоки, которые подсвечиваются в окне модели. Подсветка может иметь четыре цвета:
Зеленый - анализ доказал, что все цели доказательства действительны.
Красный - анализ оспорил цель доказательства и сгенерировал контрпример, который сфальсифицировал эту цель.
Оранжевый - анализ оспорил цель доказательства, но он не смог сгенерировать контрпример или цель доказательства осталось неопределенным. Этот результат происходит из-за:
A цели доказательства на сигнал, значение которого программное обеспечение не может управлять, для примера, блоком Constant
A цели доказательства, которая зависит от нелинейных расчетов
Цель доказательства, которая создает арифметическую ошибку, такую как деление на нуль
Автоматическое упрямство включено, и анализ, сталкивающийся с неподдерживаемым блоком, операцию которого он не понимает, но что анализ требует сгенерировать контрпример
Тайм-аут анализа
Ограничения двигателя анализа
Серый - объект модели не был частью анализа.
Выделите результаты анализа на модели примера:
В окне Сводных данных результатов для
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 указывает, что цель доказательства того, что выходной сигнал от Compare до нуль не был 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.
В таблице Цели, сфальсифицированные Контрпримерами перечислены цели доказательства, которые Simulink Design Verifier оспорил с помощью сгенерированного контрпримера. Вы можете найти цель в окне модели, нажав
Proof Objective; программа подсвечивает соответствующий блок Цель Доказательства в окне модели.В таблице Цели, сфальсифицированные Контрпримерами, в столбце Counterexample нажмите
1.
В этом разделе отображаются сведения о цели 1 доказательства и приведены сведения о контрпримере, который Simulink Design Verifier сгенерировал, чтобы опровергнуть эту цель. В этом контрпримере значения сигналов 99 фальсифицирует цель, которую вы задали используя блок Цели доказательства. То есть 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.
Из библиотеки Раковины скопируйте блок Scope в окно модели тестовой обвязки. Блок Scope позволяет вам увидеть значение сигнала, выводимого блоком Compare To Zero в вашей модели.
В окне модели тестовой обвязки соедините выходной сигнал подсистемы Test Unit с блоком Scope.
Чтобы симулировать модель тестовой обвязки, на вкладке Simulation нажмите Run.
Программа Simulink моделирует модель тестовой обвязки.
В окне модели тестовой обвязки дважды кликните блок Scope, чтобы открыть окно отображения.
Блок Scope отображает значение сигнала, выводимого блоком Compare To Zero в вашей модели. В этом примере блок Compare To Zero возвращает 0 (false) на протяжении всей симуляции, что фальсифицирует цель доказательства того, что выход блока Compare to Zero равен 1 (true). Контрпример, который поставляет блок Signal Builder, фальсифицирует цель доказательства.
Просмотр результатов анализа
Пока ваша модель остается открытой, можно просмотреть результаты последнего анализа Simulink Design Verifier в окне Сводных данных результатов.
На вкладке Design Verifier, в разделе Review Results, нажмите Results Summary. Откроется окно Сводных данных результатов (Results Summary), в котором отображаются результаты последнего анализа Simulink Design Verifier.
Для любого анализа Simulink Design Verifier из окна Сводных данных результатов можно выполнить следующие задачи.
| Задача | Для получения дополнительной информации |
|---|---|
Выделите результаты анализа на модели. | Подсвеченные результаты на модели |
Сгенерируйте детальный анализ отчет. | Отчеты Simulink Design Verifier |
Создайте модель модели тестовой обвязки, если модель тестовой обвязки уже существует, откройте ее. Если во время анализа контрпримеры не были созданы, эта опция недоступна. | Simulink Design Verifier Моделей тестовой обвязки |
Просмотрите файл данных. | Simulink Design Verifier |
Просмотрите файл журнала. | Файлы журнала Simulink Design Verifier |
После закрытия модели можно больше не просматривать результаты анализа.
Настройте доказательство примера
Измените простую модель Simulink, цель доказательства которой Simulink Design Verifier оспорил в предыдущей задаче. В частности, настройте доказательство путем добавления и настройки блока Proof Assumption:
В Командном Окне MATLAB введите
sldvlib.Откроется библиотека Simulink Design Verifier.
Откройте вложенный раздел Цели и ограничения.
Скопируйте блок Proof Assumption в свою модель.
В окно модели вставьте блок Proof Assumption между блоками Inport и Compare To Zero.
В вашей модели дважды кликните блок Proof Assumption, чтобы получить доступ к его атрибутам.
Откроется диалоговое окно параметров блоков Proof Assumption.
В Values поле введите
[-1, 0]. При доказывании свойств этой модели Simulink Design Verifier ограничивает значения сигналов, вводя блок Compare To Zero в заданную область. Если вход блока Compare to Zero всегда находится в этой области значений, то выход блока Compare to Zero всегда будет равен 1.Нажмите Apply, а затем OK, чтобы применить изменения и закрыть диалоговое окно параметров блоков Proof Assumption.
Сохраните
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 доказал цель доказательства в модели.
В разделе «Ограничения» перечислены ограничения анализа, заданные в блоке Proof Assumption.
Прокрутите назад в верхней части окна браузера. В Table of Contents нажмите
Proof Objectives Status.
В таблице «Проверенные цели» перечислены цели доказательства, которые оказались действительными для 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 искал все достижимые строения вашей модели - даже таковые, которые достигаются только после длительных задержек времени. Время расчета и память, необходимые для поиска модели, совершенно часто делают исчерпывающее доказательство непрактичным.
Доказательство свойств в больших моделях дает подробную информацию о стратегиях, которые вы можете использовать, чтобы улучшить эффективность анализа доказательства свойств большой модели.