Обнаружьте ошибки целочисленного переполнения в модели при помощи анализа поиска ошибок проектирования. Simulink® Design Verifier™ идентифицирует построения модели, которые могут привести к целочисленному переполнению и затем или доказывают, что целочисленное переполнение не может произойти в процессе моделирования или генерирует тесты, который демонстрирует ошибку целочисленного переполнения.

Найдите нарушение свойства при помощи анализа доказательства свойства Simulink® Design Verifier™. Вы моделируете требования техники безопасности как свойства и затем проверяете модель проекта по требованиям.

Сгенерируйте тесты, которые достигают полного покрытия модели. По умолчанию Simulink Design Verifier генерирует тесты, которые удовлетворяют целям на наименьшем количестве шагов. Одна из целей тестирования обеспечивает дискретный интегратор в ПИ-контроллере, чтобы превысить его верхний предел. Когда вы запускаете Simulink Design Verifier без ограничений, предел превышен на одном шаге путем принуждения скорости, чтобы быть 500. Ограничение на ограничения скорости значения в тестах между 0 и 100. Это обеспечивает тесты, чтобы взять несколько выборок, чтобы превысить предел интегратора.

Обнаружьте ошибки целочисленного переполнения в модели при помощи анализа поиска ошибок проектирования. Simulink® Design Verifier™ идентифицирует построения модели, которые могут привести к целочисленному переполнению и затем или доказывают, что целочисленное переполнение не может произойти в процессе моделирования или генерирует тесты, который демонстрирует ошибку целочисленного переполнения.

Обнаружьте из связанных ошибок доступа к массиву в модели.

Сгенерируйте тесты, которые достигают полного покрытия модели для debouncer. Результатом каждой точки покрытия модели в этой модели в качестве примера является цель тестирования. Если вы сконфигурируете Simulink Design Verifier, чтобы сгенерировать наименьшее количество тестов, это удовлетворит как можно большему количеству целей в каждом тесте.

Сгенерируйте тесты, которые удовлетворяют Решению, Условию и покрытию MCDC. Simulink Design Verifier автоматически генерирует тестовые данные и доказывает свойства моделей. Это производит последовательности входных значений, которые удовлетворяют тестированию критерии или демонстрируют контрпример доказательства. Параметры конфигурации, сопоставленные с моделью, задают цели анализа. Когда вы анализируете модель, Simulink Design Verifier использует исчерпывающие методы поиска, чтобы сгенерировать входные данные. Когда успешный, это генерирует тестовые данные и создает новую модель тестовой обвязки, содержащую блок Signal Builder со значениями данных, которые удовлетворяют аналитическим целям. ПРИМЕЧАНИЕ: сложность этой силы модели препятствует тому, чтобы генерация тестов завершилась в выделенное время. Можно остановить генерацию тестов и сгенерировать частичные результаты, или можно расширить ограничение по времени путем редактирования опций Simulink Design Verifier.

Сгенерируйте тесты, которые достигают полного покрытия модели. По умолчанию Simulink Design Verifier генерирует тесты, которые удовлетворяют целям на наименьшем количестве шагов. Одна из целей тестирования обеспечивает дискретный интегратор в ПИ-контроллере, чтобы превысить его верхний предел. Когда вы запускаете Simulink Design Verifier без ограничений, предел превышен на одном шаге путем принуждения скорости, чтобы быть 500. Ограничение на ограничения скорости значения в тестах между 0 и 100. Это обеспечивает тесты, чтобы взять несколько выборок, чтобы превысить предел интегратора.

Сгенерируйте тесты, которые достигают полного покрытия модели для триггера. Результатом каждой точки покрытия модели в этой модели в качестве примера является цель тестирования. Если вы сконфигурируете Simulink Design Verifier, чтобы сгенерировать наименьшее количество тестов, это удовлетворит как можно большему количеству целей в каждом тесте.

Найдите нарушение свойства при помощи анализа доказательства свойства Simulink® Design Verifier™. Вы моделируете требования техники безопасности как свойства и затем проверяете модель проекта по требованиям.

Проверьте свойства безопасности в модели проекта инвертора тяги. Блок Properties ниже его содержит четыре свойства безопасности. Simulink Design Verifier анализирует модель проекта и свойства безопасности доказать правильность или идентифицировать контрпримеры. Использование ссылки модели избавляет от необходимости добавлять содержимое верификации в модель проекта, позволяя содержимому верификации существовать независимо из проекта.

Выполните анализ доказательства свойства с несколькими свойствами. Модель сконфигурирована для анализа, чтобы попытаться доказать что:

Докажите свойства в алгоритме круиз-контроля фиксированной точки. Это ссылается на модель проекта с помощью модели - ссылки так, чтобы модель первоначального проекта была неизменна. Заменяющее правило блока задает свойство, которое проверяет, возможно ли переполнение. Подсистема верификации задает предположение на области значений входа скорости во время доказательства свойства. Эта модель конфигурирует Simulink Design Verifier, чтобы применить замену блока к блоку Sum, который питает выходной порт ПИ-контроллера фиксированной точки в модели, на которую ссылаются, и возвратите контрпример, который демонстрирует переполнение.

Настройки параметров с помощью конфигурационного файла параметра в анализе Simulink Design Verifier. Модель содержит параметр control_mode, который включает активный контроллер и выбирает его выход, чтобы быть выходом модели. Simulink Design Verifier обрабатывает этот параметр как вход, который ограничивается быть или 1 или 2 и генерирует соответствующее значение для каждого теста.

Временные системные требования модели для свойства, доказывающего и генерации теста с помощью блоков Simulink® Design Verifier™ Temporal Operator.

Временные системные требования модели в моделях контроллеров окна со стеклоподъемником для свойства, доказывающего и генерации теста с помощью блоков Simulink® Design Verifier™ Temporal Operator.

Сгенерируйте отчет покрытия модели путем симуляции модели тестовой обвязки с блоком Signal Editor Inputs. Можно симулировать один тест или контрпример путем выбора активного сценария в диалоговом окне Signal Editor. Для получения дополнительной информации смотрите, Симулируйте Модель тестовой обвязки при помощи редактора Инпутса Блока Сигнала.