Simulink Design Verifier
Обнаружение ошибок проектирования, доказательство свойств и генерация тестовых векторов.
Документация
Simulink Design Verifier использует формальные (математические) методы для выявления скрытых ошибок проектирования в моделях. Simulink Design Verifier обнаруживает блоки в модели, которые приводят к переполнению целых чисел, мертвой логике, нарушениям доступа к массивам и делению на ноль. Simulink Design Verifier формально проверяет, что проект соответствует функциональным требованиям. Для каждой ошибки проектирования или нарушения требований генерируется тестовый вектор для демонстрации сбойного поведения.
Simulink Design Verifier генерирует тестовые вектора для покрытия модели и пользовательских целей, чтобы расширить существующие тестовые вектора на основе требований. Тестовые вектора создаются с целью обеспечить полное покрытие модели. В дополнение к целям покрытия, можно указать собственные цели тестирования для автоматической генерации тестовых векторов на основе требований.
Поддержка отраслевых стандартов доступна в IEC Certification Kit (for ISO 26262 and IEC 61508) и DO Qualification Kit (for DO-178).
Обнаружение ошибок проектирования
Обнаружение ошибок проектирования в модели до запуска симуляций, в том числе ошибок времени выполнения, ошибок диагностики и мертвой логики.
Ошибки времени выполнения и диагностики
Обнаружение ошибок времени выполнения и моделирования, в том числе переполнения целых чисел, деления на ноль, выхода за пределы массива, ненормальных значений и ошибок операций с плавающей точки, а также ошибки достоверности данных до запуска симуляций.
Мертвая логика
Обнаружение неисполняемых конструкций модели.
Обнаружение ошибок проектирования для целочисленного переполнения (англ.)
Рабочий процесс проверки для проектирования на основе моделей с использованием Polyspace и Simulink Design Verifier (англ.)Генерация тестовых векторов
Генерация тестовых векторов для достижения целей структурного и функционального покрытия.
Тестовые вектора для увеличения покрытия
Дополнение и расширение существующих вручную созданных тестовых векторов для устранения неполного покрытия модели.
Тестовые вектора на основе требований
Генерация тестовых векторов из моделей системных требований.
Тестовые вектора для C/C++ кода
Создание тестовых векторов для увеличения покрытия сгенерированного кода и кода, вызываемого из блоков Simulink и диаграмм Stateflow.
SimulinkВерификация на основе требований
Формальная верификация требований, смоделированных с использованием MATLAB, Simulink и Stateflow.
Требования безопасности
Формальное доказательство соответствия проекта формально определенным требованиями безопасности, которые моделируются с помощью MATLAB, Simulink и Stateflow.
Упрощение вариантных моделей
Создания сокращенной модели с помощью Variant Reducer для подмножества допустимых конфигураций.
Упрощение моделей для их развертывания
Variant Reducer используется для генерации упрощенной модели для подмножества допустимых конфигураций и вариантов. Анализируются все связанные файлы и зависимые переменные. Результаты работы упаковываются в отдельную папку, что позволяет легко развертывать их и делиться ими с клиентами и партнерами.
Верификация и валидация на уровне моделей (SLVV)
