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