Формальные методы верификации и валидации (SLVV)

Курс дает практические навыки тестирования и формальной верификации моделей Simulink для разработки встраиваемых алгоритмов систем повышенной надежности.

Вы научитесь:

• Создавать тестовые вектора для моделей Simulink;
• Анализировать результаты симуляций для верификации поведения модели;
• Автоматизировать тестирование и управлять его результатами;
• Техникам формальной верификации;
• Автоматизировать получение артефактов.

Предварительная подготовка:

Настоятельно рекомендуется предварительное прохождение курсов "MATLAB для профессионалов" и "Simulink для моделирования систем и алгоритмов" или аналогичный опыт с продуктами MATLAB и Simulink.

Продолжительность курса – 1 день.

Программа курса:

Модуль 1. Верификация и валидация в модельно-ориентированном проектировании.

Модуль 2. Разработка тестовых векторов.

Модуль 3. Анализ результатов тестирования.

Модуль 4. Выполнение множественных тестов.

Модуль 5. Формальная верификация моделей.

Подробная программа курса:

Модуль 1. Верификация и валидация в Модельно-ориентированном проектировании.

В этом модуле будут рассмотрены такие базовые вопросы, как:

1. Рабочий процесс тестирования в рамках Модельно-ориентированного проектирования;
2. Непрерывная верификация и валидация;
3. Виды верификации.

В качестве примера будет рассмотрен проект электронной системы управления тягой. 

Модуль 2. Разработка тестовых векторов.

В этом модуле будет показано как создавать тестовые вектора для моделей Simulink.

1. Определение тестовых векторов;
2. Создание тестовых обвязок;
3. Создание и импорт тестовых данных;
4. Создание тестовых векторов с логикой.

Модуль 3. Анализ результатов тестирования.

В этом модуле рассматриваются такие приемы анализа результатов тестирования, как:

1. Подтверждение выполнения требований;
2. Работа с результатами тестирования: хранение, анализ и сравнение;
3. Сбор покрытия модели.

Модуль 4. Выполнение множественных тестов.

В этом модуле объясняется, как автоматизировать последовательное выполнение тестов, а также документирование результатов тестирования.

1. Создание тестовых файлов;
2. Конфигурация тестов;
3. Построение отчетов по результатам тестирования.

Модуль 5. Формальная верификация моделей.

В этом модуле рассматривается формальные методы для математического анализа моделей Simulink без тестовых векторов.

1. Использование Simulink Design Verifier;
2. Автоматическое создание тестов;
3. Доказательство свойств;
4. Обнаружение ошибок проектирования.