Определение целей, которым должны удовлетворять сигналы при проверке свойств модели
Программа Simulink Design Verifier
При работе в режиме проверки свойств программное обеспечение Simulink ® Design Verifier™ подтверждает, что свойства модели удовлетворяют заданным критериям (см. раздел Что такое проверка свойств?). В этом режиме можно использовать блоки Proof Objective для определения целей проверки для сигналов в модели.
Параметр «Значения» позволяет задать допустимые значения для входного сигнала блока. Если значение сигнала отклоняется от допустимых значений на любом временном шаге, происходит нарушение свойства и цель доказательства фальсифицируется. Блок применяет указанный параметр Values к входному сигналу, и программа Simulink Design Verifier доказывает или опровергает, что свойства модели удовлетворяют заданным критериям.
Диалоговое окно параметров блока позволяет
Включение или отключение цели.
Укажите, что блок должен отображать свой параметр «Значения» в редакторе Simulink.
Укажите, что блок должен отображать свой выходной порт.
Примечание
Программное обеспечение Simulink и Simulink Coder™ игнорируют блок Proof Objective во время моделирования модели и генерации кода соответственно. Программа Simulink Design Verifier использует блок Proof Objective только при проверке свойств модели.
Параметр Values (Значения) используется для определения значений, которые должны быть достигнуты сигналом во время моделирования проверки. Укажите любую комбинацию скаляров и интервалов в виде массива ячеек MATLAB ®. Сведения о массивах ячеек см. в разделе Массивы ячеек.
Совет
Если параметр Values указывает только одно скалярное значение, вводить его в виде массива ячеек MATLAB не требуется.
Каждое из скалярных значений содержит одну ячейку в массиве, например:
{0, 5}Замкнутый интервал содержит двухэлементный вектор в качестве ячейки в массиве, где каждый элемент определяет конечную точку интервала:
{[1, 2]}Можно также задать скалярные значения с помощью Sldv.Point конструктор, который принимает одно значение в качестве аргумента. Можно указать интервалы с помощью Sldv.Interval конструктор, который требует два входных аргумента, т.е. нижнюю и верхнюю границы для интервала. Дополнительно можно указать одно из следующих значений в качестве третьего входного аргумента, указывающего включение или исключение конечных точек интервала:
'()' - определяет открытый интервал.
'[]' - определяет замкнутый интервал.
'(]' - определяет левый открытый интервал.
'[)' - определяет интервал открытия справа.
Примечание
По умолчанию Sldv.Interval считает интервал закрытым, если опустить его третий входной аргумент.
Например, параметр Values
{0, [1, 3]}указывает:
0 - скаляр
[1, 3] - закрытый интервал
Параметр «Значения»
{Sldv.Interval(0, 1, '[)'), Sldv.Point(1)}указывает:
Sldv.Interval(0, 1, '[)') - интервал открытия справа [0, 1)
Sldv.Point(1) - скаляр
Если указать несколько скаляров и интервалов для блока Proof Objective, программа Simulink Design Verifier объединит их с помощью логической операции OR во время проверки свойств. В этом случае программное обеспечение считает, что вся цель доказательства удовлетворена, если удовлетворен какой-либо один скаляр или интервал.
Блок Proof Objective принимает сигналы всех встроенных типов данных, поддерживаемых программным обеспечением Simulink. Сведения о типах данных, поддерживаемых программным обеспечением Simulink, см. в разделе Типы данных, поддерживаемые Simulink. Блок не поддерживает сложные входные сигналы.
Укажите, включен ли блок. При выборе (по умолчанию) программа Simulink Design Verifier использует блок при проверке свойств модели. При снятии этой опции блок отключается, то есть программное обеспечение Simulink Design Verifier ведет себя так, как если бы блок Proof Objective не существовал. Если этот параметр не выбран, блок отображается в редакторе Simulink серым цветом.
Укажите цель подтверждения (см. Определение целей подтверждения).
Укажите, будет ли блок отображать содержимое своего параметра «Значения» в редакторе Simulink. По умолчанию этот параметр выбран.
Укажите, будет ли блок отображать выходной порт в редакторе Simulink. Если выбран (по умолчанию), блок отображает свой выходной порт, позволяя входному сигналу проходить как блочный выход. Если этот параметр не выбран, блок скрывает свой выходной порт и завершает входной сигнал. Следующая графика иллюстрирует внешний вид блока в каждом случае.
Стиль прохождения: Выбрано
Стиль прохождения: Отмена выбора
Укажите, следует ли останавливать моделирование, если при моделировании возникает сигнал, нарушающий свойство, указанное в параметре Values.
При выборе этого параметра и моделировании модели моделирование останавливается, если обнаруживается нарушение указанного свойства.