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