В следующих разделах описывается модель Simulink ®, для которой доказывается свойство, указанное с помощью блока Proof Objective. В этом примере демонстрируются возможности проверки свойств Simulink Design Verifier™.
В этом примере выполняются следующие задачи.
| Задача | Описание | Видишь... |
|---|---|---|
| 1 | Создайте пример модели. | |
| 2 | Убедитесь, что модель совместима с Simulink Design Verifier. | |
| 3 | Добавьте в модель блок Proof Objective, чтобы подготовить его к подтверждению. | |
| 4 | Настройте Simulink Design Verifier для проверки свойств. | |
| 5 | Докажи свойство вашей модели. | |
| 6 | Просмотрите результаты анализа. | |
| 7 | Добавьте допущения проверки, чтобы указать ограничения анализа. | |
| 8 | Докажи свойство пользовательской модели и интерпретировать результаты. |
Создайте модель Simulink для использования в следующем примере:
Создайте пустую модель Simulink.
Скопируйте следующие блоки в пустое окно модели:
Из библиотеки источников блок Inport инициирует входной сигнал, значение которого контролирует Simulink Design Verifier.
Из библиотеки Logic and Bit Operations блок Compare To Zero обеспечивает простую логику
Из библиотеки Sinks блок Outport для приема выходного сигнала
Соедините эти блоки таким образом, чтобы модель была похожа на следующую модель:
На вкладке Моделирование (Modeling) щелкните Параметры модели (Model Settings).
В диалоговом окне Параметры конфигурации (Configuration Parameters) на панели Решатель (Solver) в области Выбор решателя (Solver selection):
Задайте для параметра «Тип» значение Fixed-step.
Задайте для опции «Решатель» значение Discrete (no continuous states).
Simulink Design Verifier может анализировать только модели, использующие решатель с фиксированным шагом.
Нажмите кнопку ОК, чтобы сохранить изменения и закрыть диалоговое окно Параметры конфигурации (Configuration Parameters).
Сохраните модель с именем ex_property_proving_example_basic.
Каждый раз, когда программа Simulink Design Verifier анализирует модель, перед началом анализа программа выполняет проверку совместимости. Если модель несовместима, программа не может проанализировать ее.
Перед началом анализа можно также убедиться, что модель совместима с Simulink Design Verifier.
Откройте окно ex_property_proving_example_basic модель.
На вкладке «Проверка проекта» нажмите кнопку «Проверить совместимость».
Программа Simulink Design Verifier отображает окно журнала, в котором указывается, совместима ли модель.
Только что созданная модель совместима.
Если проверка совместимости показывает, что модель частично совместима, модель содержит по крайней мере один объект, который Simulink Design Verifier не поддерживает. Можно проанализировать частично совместимую модель, но по умолчанию неподдерживаемые объекты блокируются. Результаты анализа могут быть неполными. Дополнительные сведения об автоматическом блокировании см. в разделе Обработка несовместимости с автоматическим блокированием.
Подготовьте пример модели для подтверждения ее свойств с помощью Simulink Design Verifier. В частности, выполните монтаж модели путем добавления и конфигурирования блока Proof Objective:
В окне команд MATLAB ® введитеsldvlib.
Появится библиотека Simulink Design Verifier.
Откройте подзаголовок «Цели и ограничения».
Скопируйте блок Proof Objective в модель и вставьте его между блоками Compare To Zero и Outport.
В модели дважды щелкните блок «Proof Objective».
Откроется диалоговое окно Параметры блока проверки цели (Proof Objective block parameters).
В поле «Значения» введите 1.
Программное обеспечение Simulink Design Verifier попытается доказать, что сигнал, выводимый блоком сравнения с нулем, всегда достигает этого значения для любых сигналов, которые он принимает.
Нажмите кнопку «ОК», чтобы применить изменения и закрыть диалоговое окно «Параметры блока Proof Objective».
Сохраните модель и оставьте ее открытой.
Настройка Simulink Design Verifier для подтверждения свойств ex_property_proving_example_basic модель, которую вы внедрили:
Откройте окно ex_property_proving_example_basic модель.
На вкладке «Проверка проекта» в разделе «Режим» выберите «Проверка свойств».
Выберите «Параметры проверки свойств».
Нажмите кнопку ОК, чтобы применить изменения и закрыть диалоговое окно Параметры конфигурации (Configuration Parameters).
Примечание
На панели Проверка свойств (Property Proving) можно дополнительно указать значения для других параметров, которые управляют тем, как Simulink Design Verifier проверяет свойства модели. Дополнительные сведения см. в разделе Панель проверки проекта: проверка свойств.
Сохранить ex_property_proving_example_basic модель.
Для анализа ex_property_proving_example_basic на вкладке Design Verifier нажмите кнопку «Доказать свойства». Simulink Design Verifier начинает проверку свойств.
Во время анализа в окне журнала отображается ход выполнения анализа. Здесь отображается такая информация, как количество обработанных и удовлетворенных или сфальсифицированных целей.
Чтобы завершить анализ в любое время, в окне журнала нажмите кнопку Остановить.
По завершении анализа в окне журнала отображаются следующие опции для просмотра результатов.
Выделение результатов анализа в модели
Создание подробного отчета по анализу HTML
Создание модели кабельных трасс с тестовыми примерами
Моделирование тестовых примеров, созданных моделью, и создание отчета об охвате модели
Также можно просмотреть файл данных Simulink Design Verifier. Дополнительные сведения о файле данных см. в разделе Файлы данных Simulink Design Verifier.
В следующих разделах описывается, как можно просмотреть результаты анализа.
Результаты анализа можно просмотреть с первого взгляда, просмотрев блоки, выделенные в окне модели. Подсветка может иметь четыре цвета:
Зеленый - Анализ доказал, что все подтверждающие цели действительны.
Красный - Анализ опроверг цель доказательства и создал контрпример, который фальсифицировал эту цель.
Оранжевый - Анализ опроверг цель доказательства, но не смог создать контрпример или цель доказательства осталась неопределившейся. Этот результат возникает из-за:
Цель проверки сигнала, значение которого программное обеспечение не может управлять, например, блоком константы
Цель доказательства, которая зависит от нелинейных вычислений
Цель доказательства, создающая арифметическую ошибку, например деление на ноль
Автоматическое блокирование включено, и анализ сталкивается с неподдерживаемым блоком, чью операцию он не понимает, но анализ требует создания контрпримера
Тайм-аут анализа
Ограничения механизма анализа
Серый (Gray) - объект модели не был частью анализа.
Выделите результаты анализа в примерной модели:
В окне Сводка результатов для ex_property_proving_example_basic щелкните Подсветить результаты анализа на модели (Highlight analysis results on model).
Блок Proof Objective выделен красным цветом, что указывает на то, что цель доказательства была сфальсифицирована с помощью контрпримера.
Окно Результатов Свидетельства Дизайна Simulink появляется.
При щелчке объектов в модели это окно изменяется для отображения подробных результатов анализа для этого объекта.
Совет
По умолчанию окно Результаты Simulink Design Verifier всегда является самым видимым. Чтобы позволить окну перемещаться за другим окном, щелкните
и снимите флажок Всегда сверху.
Щелкните выделенный блок «Proof Objective».
Окно Simulink Design Verifier Results (Результаты Simulink Design Verifier Results) показывает, что цель доказательства того, что выходной сигнал из сравнения с нулем не равен 1, была опровергнута контрпримером.
Чтобы создать подробный отчет HTML-анализа:
В окне Резюме Результатов Свидетельства Дизайна Simulink нажмите отчет о подробном анализе Generate.
Отчет HTML открывается в окне браузера.
Отчет включает следующее оглавление. Щелкните гиперссылку, чтобы перейти к определенному разделу отчета.
В оглавлении щелкните Summary.
Сводка содержит обзор результатов анализа и показывает, что Simulink Design Verifier определил контрпример, который фальсифицирует цель в модели.
В оглавлении щелкните Proof Objectives Status.
В таблице Цели, сфальсифицированные контрпримерами (Targets Falsified with Counterexamples) перечислены цели доказательства, которые Simulink Design Verifier опровергла с помощью контрпримера, который она создала. Можно найти цель в окне модели, щелкнув Proof Objective; программа выделяет соответствующий блок Proof Objective в окне модели.
В таблице «Цели, сфальсифицированные контрпримерами» в столбце «Контрприбор» щелкните 1.
В этом разделе отображаются сведения о цели проверки 1 и сведения о контрпримере, созданном Simulink Design Verifier для опровержения этой цели. В этом контрпример значение сигнала 99 фальсифицирует цель, указанную с помощью блока Proof Objective. То есть 99 не меньше или равно 0, что приводит к тому, что блок Сравнить с нулем возвращает 0 (ложь) вместо 1 (истина).
Создайте модель электрического жгута с контрпримерами, которые фальсифицируют цели доказательства в модели.
В окне журнала Simulink Design Verifier щелкните Создать модель кабельных трасс.
Программа создает модель кабельных трасс с именем ex_property_proving_example_basic_harness.
Модель кабельных трасс содержит следующие элементы:
Блок построителя сигналов с именем Inputs - Группа сигналов, которые фальсифицируют цели доказательства.
Блок подсистемы с именем Test Unit - Копия модели.
DocBlock с именем Test Case Explanation - текстовое описание контрпримеров, генерируемых анализом.
A Size-Type block - подсистема, передающая сигналы от блока входов в блок блока тестирования. Этот блок проверяет, что размер и тип данных сигналов согласуются с блоком блока тестирования.
Дважды щелкните на блоке «Входные данные».
Входной сигнал 1 приводит к тому, что выходной сигнал блока сравнения с нулем равен 0. Этот контрпример нарушает цель доказательства, которая указывает, что выходной сигнал блока сравнения с нулем равен 1.
Смоделировать модель электрического жгута, чтобы увидеть контрпример, который фальсифицирует цель доказательства в модели:
Откройте окно ex_property_proving_example_basic модель.
На вкладке «Моделирование» выберите «Обозреватель библиотек».
Из библиотеки «Раковины» скопируйте блок «Область» в окно модели кабельных трасс. Блок Область (Scope) позволяет видеть значение сигнала, выводимого блоком Сравнить с нулем (Compare To Zero) в модели.
В окне модели электрического жгута подключите выходной сигнал подсистемы блока тестирования к блоку области.
Чтобы смоделировать модель электрического жгута, на вкладке Моделирование (Simulation) щелкните Выполнить (Run).
Программа Simulink моделирует модель электрического жгута.
В окне модели кабельных трасс дважды щелкните блок Область (Scope), чтобы открыть его окно отображения.
В блоке Область (Scope) отображается значение сигнала, выводимого блоком Сравнить с нулем (Compare To Zero) в модели. В этом примере блок «Сравнить с нулем» возвращает 0 (false) во время моделирования, что фальсифицирует цель доказательства того, что вывод блока «Сравнить с нулем» равен 1 (true). Контрпример, который блок Signal Builder предоставляет, фальсифицирует цель доказательства.
Пока модель остается открытой, можно просмотреть результаты последнего анализа Simulink Design Verifier в окне Сводка результатов (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 Absulation:
В окне команды MATLAB введите sldvlib.
Откроется библиотека Simulink Design Verifier.
Откройте подзаголовок «Цели и ограничения».
Скопируйте блок «Подтверждение допущения» в модель.
В окне модели вставьте блок Proof Summission между блоками Inport и Compare To Zero.
В модели дважды щелкните блок «Подтверждение допущения», чтобы получить доступ к его атрибутам.
Откроется диалоговое окно параметра блока «Подтверждение допущения».
В поле «Значения» введите [-1, 0]. При проверке свойств этой модели Simulink Design Verifier ограничивает значения сигналов, вводимые в блок «Сравнить с нулем», заданным диапазоном. Если вход блока Сравнить с нулем (Compare to Zero) всегда находится в этом диапазоне, то выход блока Сравнить с нулем (Compare to Zero) всегда будет равен 1.
Нажмите кнопку «Применить», а затем кнопку «ОК», чтобы применить изменения и закрыть диалоговое окно параметра блока «Подтверждение допущения».
Сохранить ex_property_proving_example_basic модель и держать ее открытой.
Проанализируйте модель, которую вы изменили, чтобы увидеть, как блок «Подтверждение допущения» влияет на анализ проверки свойств.
Откройте окно ex_property_proving_example_basic модель. На вкладке Design Verifier щелкните Доказать свойства.
По завершении анализа в окне журнала отображаются опции. Создание модели кабельных трасс невозможно, поскольку анализ удовлетворял всем целям проверки в модели, поэтому контрпримеров не существует.
Анализ результатов второго анализа:
Выделите модель, чтобы увидеть результаты анализа:
Щелкните Подсветить результаты анализа на модели (Highlight analysis results on model).
Теперь цель подтверждения выделена зеленым цветом.
Щелкните на блоке «Proof Objective».
Окно Результатов Свидетельства Дизайна Simulink показывает, что цель доказательства, которая указывает, что сигнал быть 1 действителен.
Просмотрите результаты анализа в подробном отчете:
Щелкните Создать подробный отчет об анализе (Generate detailed analysis report).
В оглавлении щелкните Summary.
В главе «Сводка» указано, что Simulink Design Verifier доказал свою достоверность в модели.
В разделе Ограничения (Constraints) перечислены ограничения анализа, указанные в блоке Подтверждение (Proof).
Выполните прокрутку до верхней части окна браузера. В оглавлении щелкните Proof Objectives Status.
В таблице Targets Proven Valid перечислены цели проверки, которые Simulink Design Verifier доказал.
Прокрутите вниз, чтобы просмотреть главу «Свойства», или перейдите в верхнюю часть окна браузера и в оглавлении щелкните Properties.
Сводка «Цель подтверждения» (Proof Objective) показывает, что Simulink Design Verifier доказал достижение цели, указанной в модели. Блок подтверждения допущения ограничивает область входных сигналов интервалом [-1, 0]. Поэтому программное обеспечение доказывает, что этот интервал не содержит значений, которые больше нуля, тем самым удовлетворяя цели доказательства.
Если в результате анализа возникает ошибка The model is contradictory in its current configuration, программа обнаружила противоречие в модели и не может проанализировать модель. Может возникнуть противоречие, если в модели имеются блоки Proof Absulation с неверными параметрами. Например, предположение может утверждать, что сигнал должен быть между 0 и 5, когда сигнал является постоянным 10.
Если программа обнаруживает противоречие, все предыдущие результаты признаются недействительными, и программа сообщает, что все свойства фальсифицированы.
Примечание
Ограничения, добавленные на входах либо через расчетный минимум/максимум, либо через условия испытаний/допущения, не приводят к противоречиям. Однако при ограничении сигналов, расположенных ниже по потоку от вычислений, с использованием тестовых условий/допущений проверки необходимо убедиться в том, что ограниченное условие осуществимо посредством расчета модели. В противном случае результирующая модель является противоречивой, что может привести к недействительным результатам с явной ошибкой анализа или без нее. Чтобы убедиться, что ограничения выполнимы, сначала попробуйте выполнить одно и то же условие с помощью тестовой цели. Если это условие может быть выполнено, можно безопасно использовать то же условие, что и ограничение.
Тщательное доказательство модели требует, чтобы Simulink Design Verifier искал все доступные конфигурации модели - даже те, которые достигаются только после длительных задержек. Вычислительное время и память, необходимые для поиска модели, совершенно часто делают исчерпывающее доказательство нецелесообразным.
Докажи свойства в больших моделях дает подробную информацию о стратегиях, которые вы можете использовать, чтобы улучшить производительность проверки свойств большой модели.