В этом примере показано, как моделировать временные системные требования в модели контроллера окна питания для проверки свойств и создания тестовых примеров с использованием блоков 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) Препятствие и входы конечного упора никогда не становятся истинными одновременно.
2) Препятствие не возникает несколько раз в течение следующего 1-секундного интервала.
Для временного предположения о препятствии используйте блок детектора с типом выходного сигнала «Задержанная фиксированная продолжительность», чтобы зафиксировать фиксированную продолжительность в 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 шага. Следует отметить, что ввод не наблюдается во время фазы построения выходного сигнала для детектора с типом выходного сигнала «Отложенная фиксированная длительность». В случае, когда препятствие может возникать свободно в отсутствие предположения, можно наблюдать все промежуточные вхождения препятствия. Это может быть достигнуто посредством блока расширителя с «конечной» длительностью расширения, равной 4 шагам времени.
Теперь рассмотрим функцию AutoDown контроллера окна питания.
На иллюстрации рассмотрим эту спецификацию свойства в небольших частях:
Первая интересующая временная длительность, «водитель нажимает кнопку вниз менее 1 секунды», фиксируется Detector1. При частоте выборки 0,2 1-секундный интервал разбивают на 5 временных шагов. При обнаружении понижающего сигнала Detector1 строит на своем выходе 5-ступенчатую фиксированную временную длительность, которая впоследствии будет использоваться в сочетании с другими ограничениями.
Для функции автозавершения известно, что сигнал понижения не может быть нажат в течение более 1 секунды или 5 шагов времени. Таким образом, необходимо убедиться, что и драйвер вверх и вниз являются «истинными» или оба являются «ложными» менее чем за 5 шагов после нажатия кнопки вниз. Принимая значение AND этой нейтрали драйвера и выходного сигнала детектора, установите ограничение на то, что драйвер может быть нажат в течение любого числа последовательных шагов времени менее 5.
Вы также должны убедиться, что в течение этого периода, другие сигналы, такие как препятствие, EndStop и DriverUp не соответствуют действительности, так как они будут выводить контроллер из ответа на вниз пресса. Это фиксируется с помощью Detector2 путем принудительного выполнения NOT (HaltDown) в течение 5 шагов времени. Detector2 имеет тип вывода «Отложенная фиксированная продолжительность». Он также имеет «Временные шаги для обнаружения входных данных» = 5 и «Временные шаги для длительности выходных данных» = 1.
Возьмите И этих построенных длительностей.
Для функции автозагрузки не требуется ограничивать количество шагов времени, в течение которых контроллер выдает команду отключения. Вы знаете, что вы хотите, чтобы контроллер продолжал давать команду вниз, пока драйвер не нажмет команду вверх или вниз снова, или препятствие или физический конец оконной рамы не будет поражен. Это поведение может быть зафиксировано блоком медиаприставки с «бесконечным» периодом расширения и внешним сигналом сброса, который кодирует условие завершения расширения.
Заключительная часть является блоком Imperes, который принимает временную длительность, созданную, как описано выше, и проверяет, является ли команда контроллера down верной для каждого временного шага этой длительности.
После получения этой начальной спецификации свойств ее можно использовать для проверки свойств с помощью Simulink Design Verifier. Вы получите контрпример для этого свойства. Контрпример показывает сценарий, в котором команда down дается, когда контроллер находился в аварийном состоянии down из-за реакции на ранее обнаруженное препятствие. После того как вы добавите ограничение, чтобы избежать этого, вы получите другой контрпример: если кнопка «Вниз» нажата, когда ранее была дана команда «Вверх», функция «Автозагрузка» отключена, а команда «Вниз» дана только при нажатии кнопки «Вниз». Рассматривая эти контрпримеры и наблюдая за моделью, можно увидеть образец того, что функция AutoDown включается только тогда, когда контроллер находится в нейтральном состоянии, чтобы начать с того момента, когда драйвер нажимает кнопку down.
Включите это ограничение, заставив выход контроллера быть нейтральным - ни одна из команд up или down не является истинной - в качестве предварительного условия для свойства AutoDown. Это свойство доказано.
% Valid AutoDown open_system('sldvdemo_powerwindow_vs/Verification Subsystem3')
После указания свойств в дополнение к проверке свойств можно запустить Simulink Design Verifier для автоматического создания тестовых примеров, выполняющих различные условия в свойстве. Этого можно достичь, разместив пользовательские блоки контрольных целей в соответствующих местах свойства.
Одно из таких мест для размещения блока Test Objective (со значением «true») находится на сигнале, подаваемом на первый вход блока Improts (как показано в приведенном выше свойстве). При выполнении генерации теста эта цель теста выполняется, и вы получите тестовый случай, выполняющий различные ограничения, закодированные в свойстве. Программа Simulink Design Verifier может также создать тестовый жгут для моделирования этого тестового случая. Ниже показан блок построителя сигналов с соответствующими сигналами.
Теперь можно смоделировать этот тестовый случай и посмотреть, как временные длительности создаются в свойстве, поместив область, которая отображает входные и выходные значения двух блоков и No_Cmd детектора.
Проверка значений тестового случая вручную позволяет проверить, работает ли указанное свойство по назначению.
Этот блок Test Objective помогает определить сценарий, в котором свойство является действительным, в то время как блок Improts не является тривиально верным. Блок Incompees тривиально верен, когда его выход равен true, поскольку его первый вход - false. Когда вы получаете тестовый случай, удовлетворяющий этой цели теста, вы знаете, что есть, по крайней мере, один случай, когда первый вход в блок Improts является истинным.
Это упражнение поможет проверить спецификации свойств, проверяя вручную тестовые примеры, автоматически созданные программой Simulink Design Verifier.
Чтобы завершить пример, закройте все открытые модели.
close_system('sldvdemo_TOBlocks',0); close_system('sldvdemo_powerwindowController',0); close_system('sldvdemo_powerwindow_vs',0);