#verification #formal-verification #model-checking #ctl #uppaal
Вопрос:
Добрый день, я провожу некоторые эксперименты с проверкой моделей UPPAAL, и, насколько я понимаю, когда свойство не проверяется, механизм проверки (verifyta) позволяет найти только одно из следующих:
- След
- Кратчайшая трасса (количество переходов)
- Трассировка быстрого набора (Трассировка с наименьшим относительным временем).
Это имеет большой смысл, если учесть, что проверка модели фокусируется на надежности, а не на полноте, и тот факт, что существует хотя бы одна трассировка, нарушающая определенное свойство, означает, что это свойство не удовлетворено.
Однако в контексте моего приложения мне нужно было бы найти более одного контрпримера для анализа их структуры и т. Д. В этой степени мне было интересно, существует ли возможность экстраполяции ВСЕХ возможных следов, нарушающих конкретное свойство, определенное в TCTL, с учетом ограниченного пространства поиска (т. Е. Ограничения глубины графика поиска). Кроме того, если UPPAAL не предлагает такой возможности, не могли бы вы, пожалуйста, указать мне на другие инструменты, которые могли бы ее реализовать?
Большое спасибо!
Комментарии:
1. «ВСЕ возможные следы» могут быть бесконечным множеством, если в модели есть цикл.
2. Привет, мариусм, спасибо за твой ответ. Я понимаю это, но мне было интересно , можно ли, учитывая ограниченную глубину поиска — или количество шагов в моделировании — перечислить все контрпримеры. Спасибо!
3. Uppaal не имеют этой функции, но, возможно, стоит добавить ее в качестве компонента запросу github.com/UPPAALModelChecker/UPPAAL-Meta/issues я также столкнулся с аналогичной проблемой для теста поколения, где ограничивающим фактором является охват (т. е. отчет только следы с новыми покрытие), поэтому, возможно, мы получим какое-то время, чтобы реализовать что-то вроде этого.