Доказательство свойства использует те же базовые методы в качестве поиска ошибок проектирования и генерации тестов и страдает от тех же ограничений производительности. Однако различающийся поиск ошибок проектирования или генерация тестов, вы часто не можете упрощать проблему, не ставя под угрозу валидность результатов.
Можно быстро доказать простые цели доказательства, которые не затронуты динамикой модели. Однако полное доказательство требует, чтобы Simulink® Design Verifier™ перерыл все достижимые настройки вашей модели — даже те, которые достигнуты только после долговременных задержек. Время вычисления и память, требуемая искать модель полностью часто, делают исчерпывающее доказательство непрактичным.
Существует два метода, которые можно использовать, чтобы улучшать производительность свойства, доказывающего в большой модели:
Программное обеспечение Simulink Design Verifier предлагает стратегию, которая быстро идентифицирует нарушения свойства в больших, более сложных моделях. При разработке модели анализируйте модель с помощью этой стратегии так, чтобы можно было зафиксировать любые нарушения свойства прежде, чем завершить проект.
Чтобы идентифицировать нарушения свойства модели, на панели Design Verifier > Property Proving диалогового окна Configuration Parameters, задают значение параметра Strategy как FindViolation. Когда вы используете эту стратегию, параметр Maximum violation steps становится активным так, чтобы можно было задать верхнюю границу для количества временных шагов в поиске.
Во время анализа программное обеспечение ищет только нарушения свойства в конкретном количестве временных шагов. Путем идентификации и фиксации нарушений свойства сначала, вы улучшаете производительность доказывающего свойство анализа, который использует Prove стратегия.
Если нарушение не обнаруживается, невозможно нарушить свойство с любой входной последовательностью, имеющей меньше временных шагов, чем заданный предел. Однако вы не можете доказать, что свойство верно, потому что может быть контрпример в большем количестве временных шагов, чем заданный предел.
Используйте следующий метод в доказательстве свойств в большой модели. Этот метод объединения, доказывающие и ищущие нарушения:
На панели Design Verifier > Property Proving, установленной параметр Strategy на Prove.
На панели Design Verifier используйте относительно короткое значение в параметре Maximum analysis time, таком как 5–10 минут. Если тривиальные контрпримеры существуют — или если ваши свойства не зависят от динамики модели — анализ должен завершиться за то количество времени.
Измените параметр Strategy в FindViolation, и выберите маленькое направляющееся в параметр Maximum violation steps, такой как 4, 5, или 6. Если ваши свойства имеют простые контрпримеры, программное обеспечение должно обнаружить их.
Если вы не находите нарушения с маленьким связанными, увеличиваете связанное и ищете более длинные контрпримеры.
Увеличьте связанное с несколькими шагом и наблюдайте время вычислений и потребление памяти. Системные ресурсы могут ограничить продолжительность нарушения, которое может искаться.
Кроме того, считайте динамику своей модели и количество временных шагов требуемыми к переходу между произвольной парой настроек. Если вы выбираете связанное слишком большое, поиск нарушения может быть более комплексным, чем неограниченное доказательство.
Если можно запустить поиски нарушения с относительно большими границами, например, 30–50 временных шагов, переключиться назад на Prove стратегия и использование более долгое ограничение по времени, такое как несколько часов.
