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