Степень временных свойств контроллера окна
Этот пример показывает, как смоделировать требования временной системы в моделях контроллеров окна со степенью для проверки свойств и генерации теста с помощью блоков Simulink ® Design Verifier™ Temporal Operator.
Темпоральные операторы
Библиотека Simulink ® Design Verifier™ предоставляет три основных темпорального оператора, которые могут использоваться для моделирования временных свойств. Целью темпоральных операторов является поддержка спецификации временных требований, так что смоделированное свойство имеет более близкую корреляцию с фактическим текстовым требованием. Эти блоки являются низкоуровневыми базовыми блоками для построения более сложных временных свойств.
Контроллер Окна со степенью
Контроллер окна со степенью реагирует на команды драйвера и пассажира, выдавая команды для перемещения окна вверх или вниз. Он также реагирует на препятствие и на достижение конца системы координат в любом направлении.
Примите во внимание следующие два требования к контроллеру окна со степенью:
Требование 1 (реакция на препятствия)
Каждый раз, когда обнаруживается препятствие, контроллер выдает команду на понижение в течение 1 секунды.
Требование 2 (функция автозапуска)
Если драйвер нажимает кнопку «вниз» менее 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')
Глобальные допущения: Контроллер окна со степенью является открытой системой. Это делает среду, управляемую входами, препятствием и конечной остановкой (конец оконной системы координат), происходить свободно. Чтобы ограничить окружение, добавьте два глобальных предположения для моделей контроллеров.
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 с выходом «Delayed Fixed Duration» для спецификации свойства. После обнаружения препятствия создайте фиксированный интервал в 4 шага. Обратите внимание, что вход не наблюдается во время фазы конструкции выхода для детектора с типом вывода «Отложенная фиксированная длительность». В случае, когда препятствие может возникнуть свободно в отсутствие предположения, вы, возможно, захотите наблюдать все промежуточные вхождения препятствия. Это может быть достигнуто через блок Extender с «длительность в 4 временных шага.
Теперь рассмотрим функцию AutoDown контроллера окна со степенью.
Для рисунка рассмотрим эту спецификацию свойств в небольших частях:
Первая интересующая временная длительность, «драйвер нажимает кнопку опускания менее 1 секунды», захватывается Detector1. При скорости дискретизации 0,2 1-секундный интервал разбивается на 5 временных шагов. При обнаружении понижающего сигнала Detector1 создает 5-ступенчатую фиксированную временную длительность на его выходе, которую вы впоследствии будете использовать в комбинации с другими ограничениями.
Для функции AutoDown известно, что понижающий сигнал нельзя нажимать более 1 секунды или 5 временных шагов. Таким образом, вы хотите убедиться, что оба драйвера вверх и вниз «true» или оба «false» менее чем за 5 шагов после нажатия вниз. Взяв И этого драйвера нейтраль и выход детектора, усильте ограничение, что драйвер вниз может быть нажат на любое количество последовательных временных шагов менее 5.
Также необходимо убедиться, что в течение этого периода другие сигналы, такие как препятствие, EndStop и DriverUp, не соответствуют действительности, поскольку они выведут контроллер из ответа на нажатие вниз. Это фиксируется с помощью Detector2 путем принудительного применения NOT (HaltDown) для 5 временных шагов. Detector2 имеет выходной тип «Delayed Fixed Duration». Он также имеет «Временные шаги for input detection» = 5 и «Временные шаги for output duration» = 1.
Возьмите И этих построенных длительности.
Для функции AutoDown не требуется ограничивать количество временных шагов, для которых контроллер выдает команду down. Вы знаете, что хотите, чтобы контроллер продолжал выдавать команду down, пока драйвер не нажимает команду up или down снова, или препятствие или физический конец системы координат не попадает. Это поведение может быть получено блоком Extender с периодом расширения «Infinite» и внешним сигналом сброса, который кодирует условие, чтобы закончить расширение.
Конечная часть является блоком Implices, который принимает временную длительность, сконструированную как объяснено выше, и проверяет, верна ли команда контроллера вниз для каждого временного шага этой длительности.
Если у вас есть эта начальная спецификация свойств, вы можете использовать ее для проверки свойств с помощью Simulink Design Verifier. Вы получите контрпример для этого свойства. Контрпример показывает сценарий, в котором команда down выдается, когда контроллер находился в аварийном состоянии down из-за реакции на ранее обнаруженное препятствие. После того, как вы добавите ограничение, чтобы избежать этого, вы получите еще один контрпример: если кнопка «вниз» нажата, когда была задана команда «вверх», функция «АвтоВниз» отключается, и команда «вниз» выдается только при условии, что кнопка «вниз» нажата. Глядя на эти контрпримеры и наблюдая модель, можно увидеть шаблон, который включен функцией AutoDown только, когда контроллер находится в нейтральном состоянии, чтобы начать с, когда драйвер нажимает кнопку отключения.
Включите это ограничение, заставив контроллер выход быть нейтральным - ни вверх, ни вниз команда не верна - в качестве предусловия для свойства AutoDown. Это свойство признано допустимым.
% Valid AutoDown open_system('sldvdemo_powerwindow_vs/Verification Subsystem3')
Тест для валидации свойств
Если свойства заданы, в дополнение к проверке свойств можно запустить Simulink Design Verifier, чтобы автоматически сгенерировать тесты, которые используют различные условия в свойстве. Это может быть достигнуто путем размещения пользовательских блоков Цель Тестирования в соответствующих местоположениях свойства.
Одно из таких местоположений для размещения блока Цель Тестирования (со значением «true») находится на сигнале, поступающем в первый вход блока Implices (как показано в приведенном выше свойстве). При запуске генерации тестов эта цель тестирования удовлетворяется, и вы получите контрольный пример, реализующий различные ограничения, закодированные в свойстве. Simulink Design Verifier может также создать тестовую обвязку для симуляции этого теста. Блок Signal Builder с соответствующими сигналами показан ниже.
Теперь можно симулировать этот тест и увидеть, как временные длительности создаются в свойстве, путем размещения возможностей, которая отображает входные и выходные значения двух блоков Detector и No_Cmd.
Проверка значений тестов вручную позволяет увидеть, ведет ли заданное свойство себя должным образом.
Эта цель тестирования помогает в идентификации сценария, где свойство верно, в то время как блок Implices не является тривиально верным. Блок Подразумевает, тривиально верен, когда его выход равен true из-за того, что его первый вход равен false. Когда вы получаете контрольный пример, удовлетворяющий этой цели тестирования, вы знаете, что существует, по крайней мере, один случай, когда первый вход в блок Implices равен true.
Это упражнение может помочь вам подтвердить спецификации свойств, вручную осмотрев тесты, автоматически сгенерированные Simulink Design Verifier.
Очистка
Чтобы завершить пример, закройте все открытые модели.
close_system('sldvdemo_TOBlocks',0); close_system('sldvdemo_powerwindowController',0); close_system('sldvdemo_powerwindow_vs',0);