В этом примере показано, как смоделировать временные системные требования в моделях контроллеров окна со стеклоподъемником для доказательства свойства и генерации теста с помощью блоков Simulink® Design Verifier™ Temporal Operator.
Библиотека Simulink® Design Verifier™ обеспечивает три основных блока темпорального оператора, которые могут использоваться, чтобы смоделировать временные свойства. Намерение темпоральных операторов состоит в том, чтобы поддержать спецификацию временных требований, таких, что смоделированное свойство имеет более близкую корреляцию к фактическому текстовому требованию. Эти блоки являются низкоуровневыми базовыми блоками для построения более комплексных временных свойств.
Контроллер окна со стеклоподъемником отвечает на драйвер и пассажирские команды путем предоставления команд для продвижения окна или вниз. Это также отвечает на препятствие и к достижению конца рамки окна в любом направлении.
Рассмотрите следующие два требования для контроллера окна со стеклоподъемником:
Требование 1 (ответ препятствия)
Каждый раз, когда препятствие обнаруживается, контроллер должен дать вниз команда в течение 1 секунды.
Требование 2 (функция AutoDown)
Если драйвер нажимает вниз кнопка меньше 1 секунды, контроллер продолжает давать вниз команда, пока конец не был достигнут, или драйвер нажимает кнопка.
%Model of the power window controller open_system('sldvdemo_powerwindowController') open_system('sldvdemo_powerwindowController/control')
Система верификации окна со стеклоподъемником является моделью верхнего уровня, которая содержит модель - ссылку к моделям контроллеров окна со стеклоподъемником, задающим поведение контроллера и смоделированные требования.
%Model of the top-level verification system open_system('sldvdemo_powerwindow_vs')
Глобальные Предположения: контроллер окна со стеклоподъемником является открытой системой. Это делает управляемые входные параметры среды, препятствие и endstop (конец рамки окна), чтобы произойти свободно. Чтобы ограничить среду, добавьте два глобальных предположения для своих моделей контроллеров.
1) Препятствие и входные параметры endstop никогда не становятся верными одновременно.
2) Препятствие не происходит многократно в следующем 1 втором интервале.
Для временного предположения на препятствии используйте блок Detector с выходным типом "Задержанной Фиксированной Длительности", чтобы получить фиксированную длительность 1 секунды (5 временных шагов с 0,2 шагами расчета).
% Global Assumptions open_system('sldvdemo_powerwindow_vs/Global Assumptions')
Теперь рассмотрите первое требование контроллера для Ответа Препятствия.
% Obstacle Response open_system('sldvdemo_powerwindow_vs/Verification Subsystem2')
Здесь, используйте блок Detector с выходным типом "Задержанной Фиксированной Длительности" для спецификации свойства. После обнаружения препятствия создайте фиксированный интервал 4 шагов. Обратите внимание на то, что вход не наблюдается во время выходного этапа строительства для Детектора с "Delayed Fixed Duration" тип выхода. В случае, где препятствие может произойти свободно в отсутствие предположения, вы можете хотеть наблюдать все промежуточные случаи препятствия. Это может быть достигнуто через блок расширителя с "Конечной" дополнительной длительностью 4 временных шагов.
Теперь рассмотрите функцию AutoDown контроллера окна со стеклоподъемником.
Для рисунка рассмотрите эту спецификацию свойства в меньших частях:
Первая временная длительность интереса, "драйвер нажимает вниз кнопка меньше 1 секунды", получена Detector1. На уровне частоты дискретизации 0,2, 1 второй интервал разломан на 5 временных шагов. На обнаружении вниз сигнала, Detector1 создает фиксированную временную длительность с 5 шагами при своем выходе, который вы будете впоследствии использовать в сочетании с другими ограничениями.
Для функции AutoDown вы знаете, что вниз у сигнала нельзя потребовать больше 1 секунды, или 5 временных шагов. Таким образом вы хотите гарантировать, что оба драйвера вверх и вниз "верны", или оба являются "ложными" меньше чем на 5 шагах после того, как вниз нажимается. Путем взятия AND этого нейтрального драйвера и Detector выход, осуществите ограничение, что у драйвера вниз можно потребовать любого количества последовательных временных шагов меньше чем 5.
Также необходимо гарантировать, что в этот период другие сигналы, такие как препятствие, EndStop и DriverUp не верны, поскольку они вынут контроллер из ответа к вниз нажатие. Это получено с помощью Detector2 путем осуществления этого НЕ (HaltDown), верно для 5 временных шагов. Detector2 имеет "Delayed Fixed Duration" тип выхода. Это также имеет "Временные шаги для входного обнаружения" = 5 и "Временные шаги на выходное время" = 1.
Возьмите AND этой созданной длительности.
Для функции AutoDown вы не хотите ограничивать количество временных шагов, для которых контроллер дает вниз команда. Вы знаете, что хотите, чтобы контроллер продолжил давать вниз команда, пока драйвер не нажимает или вниз команда снова, или препятствие или физический конец рамки окна не поражены. Это поведение может быть получено блоком расширителя с периодом расширения "Бога" и внешним сигналом сброса, который кодирует условие закончить расширение.
Итоговая часть является блоком Implies, который берет временную длительность, созданную, как объяснено выше и проверки, если контроллер вниз команда верен для каждого временного шага этой длительности.
Если у вас есть эта начальная спецификация свойства, можно использовать ее в свойстве, доказывающем с Simulink Design Verifier. Вы получите контрпример для этого свойства. Контрпример показывает сценарий, где вниз команда дана, когда контроллер был в чрезвычайном неработоспособном состоянии из-за ответа на более раннее обнаруженное препятствие. После того, как вы добавите ограничение, чтобы избежать этого, вы получите другой контрпример: если вниз кнопка нажимается, когда ранее команда давалась, опция AutoDown отключена и вниз, команда дана только пока вниз, кнопка нажимается. Смотря на эти контрпримеры и наблюдение модели, вы видите шаблон, что опция AutoDown активирована только, когда контроллер находится в нейтральном состоянии для начала, когда драйвер нажимает вниз кнопка.
Включите это ограничение путем принуждения контроллера выход, чтобы быть нейтральными - ни, ни вниз команда верна - как предусловие для свойства AutoDown. Это свойство доказано допустимым.
% Valid AutoDown open_system('sldvdemo_powerwindow_vs/Verification Subsystem3')
Если свойства заданы, в дополнение к доказательству свойства, можно запустить Simulink Design Verifier, чтобы автоматически сгенерировать тесты, которые осуществляют различные условия в свойстве. Это может быть достигнуто путем размещения пользовательских блоков Цели тестирования в соответствующих местоположениях в свойстве.
Одно такое местоположение, чтобы поместить блок Test Objective (с "истинным" значением) находится на сигнале, питающемся в первый вход блока Implies (как показано в вышеупомянутом свойстве). При выполнении генерации тестов удовлетворяют этой Цели тестирования, и вы получите тест, осуществляющий различные ограничения, закодированные в свойстве. Simulink Design Verifier может также создать тестовую обвязку, чтобы симулировать этот тест. Блок Signal Builder с соответствующими сигналами показывают ниже.
Можно теперь симулировать этот тест и видеть, как временная длительность создается в свойстве путем размещения осциллографа, который отображает значения ввода и вывода двух блоков Детектора и No_Cmd.
Вручную осмотр значений теста позволяет вам видеть, ведет ли заданное свойство себя, как предназначено.
Этот блок Test Objective помогает в идентификации сценария, где свойство допустимо, в то время как блок Implies не тривиально верен. Блок Implies тривиально верен, когда его выход верен из-за его первого входа, являющегося ложным. Когда вы получаете тест, удовлетворяющий этой Цели тестирования, вы знаете, что существует по крайней мере один случай, где первый вход с блоком Implies верен.
Это осуществление может помочь вам подтвердить свои спецификации свойства путем ручного осмотра тестов, автоматически сгенерированных Simulink Design Verifier.
Чтобы завершить пример, закройте все открытые модели.
close_system('sldvdemo_TOBlocks',0); close_system('sldvdemo_powerwindowController',0); close_system('sldvdemo_powerwindow_vs',0);
