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