Анализ простой модели
Эта простая модель включает два блока 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 выход. A true выводить результаты, когда вход true, и выход блока Memory следующий true. Генерация теста следует пути, чтобы достичь этого условия, которое зависит от начальных условий модели:
Если начальное значение памяти
true, тест является одним временным шагом, где входtrue.Если начальное значение памяти
false, тест является двумя временными шагами:Входное значение
trueи значение памяти ложно (строка 2). Таким образом, выход блока XORtrue, делая значение памятиtrue.Теперь вход значение и значение памяти
true(строка 4), выводитсяtrue, и анализ достигает цели тестирования.
Бесконечное число тестов может привести к тому, что вывод будет равен true, и независимо от значения состояния, выход может удерживаться ложным в течение произвольного момента времени, прежде чем делать его верным. Когда Simulink® Проектируйте Verifier™ ищет, он возвращает первый тест, который удовлетворяет цели. Этот случай неизменно является симуляцией с наименьшим количеством временных шагов. Иногда вы можете найти этот результат нежелательным, потому что это нереально или не удовлетворяет некоторым другим требованиям теста.
Те же основные принципы из этого примера применяются к доказательству свойств и генерации теста. Во время генерации теста параметры опции явно задают критерии поиска. Например, можно задать, что Simulink Design Verifier находит пути для всех выходов блоков или находит только те пути, которые приводят к тому, что вывод блоков равен true.
Во время анализа доказательства свойств вы задаете функциональное требование или свойство, которое должно быть доказано Simulink Design Verifier, для примера, что выход всегда верен. Если поиск завершается, не найдя путь, который нарушает свойство, свойство проверяется. Если программа находит путь, где выход равен false, она создает контрпример, который заставляет выход быть ложным.
Во время анализа выявления ошибок Simulink Design Verifier определяет цели, где переполнение данных или ошибки деления на нули могут и не могут возникнуть. Анализ создает тесты, которые демонстрируют, как могут возникнуть ошибки.