Эта простая модель включает два блока логических операторов и блок памяти. Постоянная информация в этой модели ограничена логическим значением блока памяти. Входным значением модели является одно логическое значение. В следующей таблице описано полное поведение модели, включая поведение, которое является результатом произвольно длинной последовательности входных данных.
| # | Вход | Значение памяти | Выход блока исключающее ИЛИ = следующее значение памяти | Выход блока И |
|---|---|---|---|---|
| 1 | false | false | false | false |
| 2 | true | false | true | false |
| 3 | false | true | true | false |
| 4 | true | true | false | true |
Целью теста является создание тестовых примеров, которые приводят к true выход. A true выходные результаты, когда входные данные true, и выходной сигнал блока памяти true. Создание тестового случая следует по пути достижения этого условия, которое зависит от исходных условий модели:
Если начальное значение памяти true, тестовый случай является одним временным шагом, где вход true.
Если начальное значение памяти false, тестовый случай представляет собой два временных шага:
Входное значение: true и значение памяти равно false (строка 2). Таким образом, выходной сигнал блока исключающее ИЛИ равен true, создание значения памяти true.
Теперь, когда входное значение и значение памяти оба true (строка 4), выходной сигнал: true, и анализ достигает цели теста.
Бесконечное число тестовых случаев может привести к тому, что выходной сигнал станет истинным, и независимо от значения состояния, выходной сигнал может оставаться ложным в течение произвольного времени, прежде чем сделать его истинным. При поиске в Simulink ® Design Verifier™ возвращается первый тестовый случай, удовлетворяющий поставленной цели. Этот случай неизменно является моделированием с наименьшим временем шагов. Иногда этот результат может оказаться нежелательным, поскольку он нереалистичен или не удовлетворяет каким-либо другим требованиям теста.
Те же основные принципы, что и в этом примере, применимы к проверке свойств и созданию тестовых примеров. Во время создания тестового случая параметры опции явно определяют критерии поиска. Например, можно указать, что Simulink Design Verifier находит пути для всех выводов блока или только те пути, по которым вывод блока становится истинным.
Во время анализа проверки свойств необходимо указать функциональное требование или свойство, для которого Simulink Design Verifier должен, например, доказать, что результат всегда верен. Если поиск завершается без поиска пути, нарушающего свойство, свойство доказывается. Если программа находит путь, по которому вывод имеет значение false, она создает контрпример, который приводит к тому, что вывод имеет значение false.
Во время анализа обнаружения ошибок Simulink Design Verifier определяет цели, в которых могут и не могут возникать ошибки переполнения данных или деления на ноль. В результате анализа создаются тестовые примеры, демонстрирующие возможные ошибки.