В этом примере показано, как смоделировать временные системные требования для доказательства свойства и генерации теста с помощью блоков Simulink® Design Verifier™ Temporal Operator.
Библиотека Simulink® Design Verifier™ обеспечивает, три основных блока темпорального оператора могут использоваться, чтобы смоделировать временные свойства. Намерение темпоральных операторов состоит в том, чтобы поддержать спецификацию временных требований, таких, что смоделированное свойство имеет более близкое co-отношение к фактическому текстовому требованию. Эти блоки являются низкоуровневыми базовыми блоками для построения более комплексных временных свойств.
Рассмотрите debounce логику что debounces между значениями 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 из Библиотеки Блоков Темпорального оператора. При обнаружении, что входное значение 1 для 7 (или больше чем 6) временные шаги, вы хотите проверять, что выход равняется 2, пока вход остается равным 1 после обнаружения. Используйте "Синхронизируемую" опцию блока Detector, сопровождаемого блоком Implies, чтобы получить это.
open_system('sldvdemo_debounce_to/Verify True Output1')
Несколько блоков темпорального оператора могут быть объединены, чтобы создать более комплексные временные свойства. Рассмотрите Требование 2.
open_system('sldvdemo_debounce_to/Verify True Output2')
Для рисунка это требование сломано примерно в три части интереса:
После того, как выход равнялся 2: Это - условие включения для вашего свойства. При проверке остальной части ограничений вы хотите знать, было ли это условие верно в какой-то момент в прошлом. Этот тип условия включения обычно сопровождается расширителем (или "Конечный" или "Бог"), что, в сочетании с другими ограничениями, может сформировать первый вход к вашему значению.
Вход становится 0 больше чем для 5 шагов, и проверяйте что-то, пока вход остается 0: По той же причине как первое свойство вы используете Детектор с "Synchronized" выход ("Временные шаги для входного обнаружения" = 6).
Выход должен равняться 1: Это - условие, которое вы хотите проверить каждый раз, когда первые два ограничения содержат. Это получено через логический блок Implies. Обратите внимание на то, что вы не можете использовать блок Within Implies здесь.
Если временные требования были смоделированы, можно выполнить свойство, доказывающее на них с помощью Simulink Design Verifier.
Чтобы завершить пример, закройте все открытые модели.
close_system('sldvdemo_TOBlocks',0); close_system('sldvdemo_debounce_to',0);