Этот пример показывает, как смоделировать требования временной системы для проверки свойств и генерации тестов с помощью блоков Simulink ® Design Verifier™ Temporal Operator.
Библиотека Simulink ® Design Verifier™ предоставляет три основных темпорального оператора, которые могут использоваться для моделирования временных свойств. Цель темпоральных операторов состоит в том, чтобы поддержать спецификацию временных требований, таким образом, чтобы смоделированное свойство было более тесно связано с фактическим текстовым требованием. Эти блоки являются низкоуровневыми базовыми блоками для построения более сложных временных свойств.
Рассмотрим логику debounce, которая разворачивается между значениями 0 и 1 на основе входного значения, удерживающего значение для фиксированного количества временных шагов.
Функциональность debounce получена на содержащей диаграмме Stateflow ®.
open_system('sldvdemo_debounce_to') open_system('sldvdemo_debounce_to/debounce')
Рассмотрим два требования модели debounce, которые вы хотели бы проверить.
Требование 1:
Каждый раз, когда вход равен 1 для более чем 6 шагов, выход должен быть равен 2.
Требование 2:
Всякий раз, когда вход становится 0 на более чем 5 шагов после выхода был 2, выход должен равняться 1, пока вход остается на 0.
Для задания Требования 1 вы сначала представляете ограничение, которое равняется 1 для более чем 6 шагов. Это может быть получено блоком Detector из библиотеки Темпорального оператора Blocks. При обнаружении, что входное значение составляет 1 для 7 (или более 6) временных шагов, вы хотите проверить, что выходное значение равняется 2, пока вход остается равным 1 после обнаружения. Используйте опцию «Synchronized» блока Detector, за которым следует блок Implies, чтобы захватить это.
open_system('sldvdemo_debounce_to/Verify True Output1')
Несколько блоков темпорального оператора могут быть объединены, чтобы создать более сложные временные свойства. Примите во внимание требование 2.
open_system('sldvdemo_debounce_to/Verify True Output2')
Для рисунка, это требование разбито примерно на три части интереса:
После выхода было 2: Это разрешающее условие для вашего свойства. При проверке остальных ограничений необходимо знать, было ли это условие верным в какой-то момент прошлого. За этим типом разрешающего условия обычно следует Extender (либо «Конечный», либо «Бесконечный»), который в сочетании с другими ограничениями может сформировать первый вход в ваше подразумеваемое значение.
Вход становится 0 более 5 шагов и проверяет что-то, пока вход остается 0: По той же причине, что и первое свойство, вы используете Детектор с выходом «Synchronized» («Временные шаги for input detection» = 6).
Значение выхода должно равняться 1: Это условие, которое вы хотите проверить каждый раз, когда держатся первые два ограничения. Это захватывается через логический блок Implices. Обратите внимание, что здесь нельзя использовать блок В Подразумевает.
После моделирования временных требований можно выполнить проверку свойств с помощью Simulink Design Verifier.
Чтобы завершить пример, закройте все открытые модели.
close_system('sldvdemo_TOBlocks',0); close_system('sldvdemo_debounce_to',0);