Моделирование требований
Блоки
| Proof Assumption | Ограничьте значения сигналов при доказывании свойств модели |
| Proof Objective | Задайте цели, которые сигналы должны удовлетворять при доказывании свойств модели |
| Assertion | Проверяйте, является ли сигнал нулем |
| Detector | Определите истинную длительность на входе и создайте выходную истинную длительность на основе типа выхода |
| Extender | Удлините истинную длительность входа |
| Implies | Задайте условие, которое создает определенный ответ |
| Within Implies | Проверьте, что реакция происходит в течение требуемой длительности |
| Verification Subsystem | Укажите доказательства или цели тестирования, не влияя на результаты симуляции или сгенерированный код |
Функции
sldv.assume | Функция доказывания допущения для диаграмм и Блоков MATLAB function Stateflow |
sldv.prove | Цель доказательства функции для диаграмм Stateflow и блоков MATLAB Function |
sldvextract | Извлеките содержимое подсистемы или субдиаграммы в новую модель для анализа |
sldvoptions | Создайте объект опций верификации проекта |
sldvrun | Анализируйте модель |
sldvreport | Сгенерируйте отчет Simulink Design Verifier |
Темы
Краткий обзор свойств проверки.
Рабочий процесс для проверки свойств модели
Очерчивает процесс доказывания свойств вашей модели.
Доказательство свойств в модели
Предоставляет пример, который проходит вас через процесс доказательства свойств модели.
Докажите свойства уровня системы с помощью модели верификации
Пример, который использует модель верификации, чтобы доказать свойства уровня системы.
Доказательство свойств в подсистеме
Объясняет, как доказать свойства в подсистеме.
Отладка свойств, доказывающих нарушения при помощи SLICER модели
Отлаживайте свойства, доказывающие нарушения, используя Model Slicer
Проектирование и проверка свойств в модели
Можно использовать Verifier™ Simulink ® Design, чтобы смоделировать требования проекта как свойства, а затем доказать свойства в модели .
Значения ограничений параметров
Обзор строения параметра для Simulink® Design Verifier™ анализ.
Библиотека блоков Simulink Design Verifier включает вложенные свойства примера.
Задайте значения ограничений для параметров
Пример того, как задать параметры как переменные для анализа.
Задайте значения ограничений параметров для полного покрытия
Пример того, как задать значения ограничений параметра для достижения полного покрытия модели.
Проект Панели верификатора: проверка свойств
Задайте опции, которые управляют тем, как Simulink Design Verifier доказывает свойства для моделей, которые он анализирует.
Проект Панели верификатора: параметры
Задайте опции, которые управляют тем, как Simulink Design Verifier использует строения параметров при анализе моделей.
Проверьте результаты анализа в окне Simulink Design Verifier Results Summary.
Что такое модель спецификации?
Обзор модели спецификации и ее использование в верификации на основе требований.
Изолируйте логику верификации с наблюдателями
Описывает поддержку наблюдателя для верификатора проекта simulink.
