В этом примере показано, как использовать блок Ссылка для выполнения анализа доказательства свойств с несколькими свойствами, не внося изменений в модель. В этом примере вы заменяете существующую подсистему верификации блоком Observer Reference. Однако можно добавить блок Ссылка к модели, даже если у вашей модели нет подсистемы верификации для замены. Для получения дополнительной информации смотрите Доступ к данным Моделям Беспроводной при Помощи Наблюдателей (Simulink Test).
Модель sldvdemo_debounce_validprop
сконфигурирован для анализа и пытается доказать, что:
Когда текущее и шесть предыдущих входных значений равны true, выход будет равен true.
Когда текущее и шесть предыдущих входных значений ложны, выход будет ложным.
Подробное описание блока Ссылка см. в разделе Изоляция логики верификации с наблюдателями.
The sldvdemo_debounce_validprop
модель содержит подсистему верификации под названием Verify Output. Дополнительные сведения о Подсистеме верификации см. в разделе Подсистема верификации. Чтобы открыть модель, введите:
open_system('sldvdemo_debounce_validprop');
Выполните эти шаги, чтобы создать новый блок Ссылка и заменить подсистему Verify Output verification.
1. Щелкните правой кнопкой мыши подсистему Verify Output. В контекстном меню выберите Наблюдатели > Переместить выбранный блок в Наблюдатель > Создать Наблюдатель.
2. Нажмите Да в появившемся диалоговом окне.
3. Блок Ссылка заменяет подсистему верификации. Откроется модель sldvdemo_denounce_validprop_Observer1| Observer.
4. Сохраните sldvdemo_debounce_validprop_Observer1
в папке с возможностью записи в пути MATLAB.
5. Дважды кликните один из блоков Observer Port, чтобы открыть окно Manage Observer Block. Два сигнала, debounce и raw, автоматически сопоставлены с двумя блоками Observer Port в sldvdemo_debounce_validprop_Observer1
Модель наблюдателя.
Чтобы выполнить анализ доказательства свойств, выполните следующие шаги:
1. В модели верхнего уровня на вкладке Design Verifier нажмите «Доказать свойства».
2. После завершения анализа окно Simulink Design Verifier Сводные Данные сообщает, что выполняются две цели.
3. Откройте отчет анализа HTML, чтобы увидеть подробный отчет, содержащий информацию о модели верхнего уровня и наблюдателях.
Отчет об анализе показывает информацию о свойствах Observer в разделе Моделей (Моделей ) (ов) Observer главы Properties.
Закройте модель.
bdclose('all');