Анализируйте простую модель
Эта простая модель включает два блока Logical Operator и блок Memory. Персистентная информация в этой модели ограничивается булевым значением блока Memory. Вход к модели является одним булевым значением. Следующая таблица описывает полное поведение модели, включая поведение, которое следует из произвольно длинной последовательности входных параметров.
| # | Входной параметр | Значение памяти | Выход блока 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 идентифицирует цели, где переполнение данных или ошибки деления на нуль могут и не могут произойти. Анализ создает тесты, которые демонстрируют, как ошибки могут произойти.