Доказательство свойств использует те же базовые методы, что и поиск ошибок проектирования и генерация тестов, и страдает от тех же ограничений эффективности. Однако, в отличие от поиска ошибок проектирования или тестовой генерации, вы часто не можете упростить задачу, не ставя под угрозу валидности результатов.
Можно быстро доказать простые цели доказательства, которые не затронуты динамикой модели. Однако тщательное доказательство требует, чтобы Simulink® Design Verifier™ просматривайте все достижимые строения вашей модели - даже таковые, которые достигаются только после длительных задержек времени. Время расчета и память, необходимые для поиска модели, совершенно часто делают исчерпывающее доказательство непрактичным.
Существует два метода, которые можно использовать, чтобы улучшить эффективность доказывания свойств в большой модели:
Программное обеспечение Simulink Design Verifier предлагает стратегию, которая быстро выявляет нарушения свойств в больших, более сложных моделях. При разработке модели анализируйте модель с помощью этой стратегии, чтобы можно было исправить любые нарушения свойств перед доработкой проекта.
Чтобы идентифицировать нарушения свойств модели, на панели Design Verifier > Property Proving диалогового окна Параметры конфигурации задайте значение параметра 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 стратегия и использовать более длительный предел, например несколько часов.
