Экспертная оценка результатов верификации инструментов верификации моделей программ

При проверке программ на соответствие спецификациям требований инструменты верификации моделей программ могут выдавать различные результаты верификации. Среди них вердикты, свидетельства нарушений и отчеты о покрытии кода представляют собой наибольшую ценность с точки зрения экспертов, которые хотят обнаружить ошибки в программах и оценить полноту проверки. Для индустриального использования инструментов верификации моделей программ, когда проверяется множество различных требований к различным версиям и конфигурациям многих программ, экспертам необходимы удобные средства автоматизации оценки результатов верификации. В статье рассматриваются соответствующие подходы и их реализация в системе верификации Klever.