Один из наиболее надежных способов проверки системы на соответствие ее спецификации – формальная верификация, а именно, метод проверки моделей. Однако, в случае наличия ошибки, для её локализации в модели пользователю необходимо самостоятельно анализировать контрпример, который представляет собой последовательность состояний всей системы. Это сложно, требует времени и усилий. Разработанное программное средство Oeritte упрощает описанную задачу. Оно содержит функциональность для визуализации контрпримера на диаграмме функциональных блоков, отображает объяснения для любого значения любой переменной на любом шаге контрпримера, а также включает в себя алгоритм и визуализацию объяснения значения проверяемой LTL формулы.
Овсянникова П.А. (науч. рук. Чивилихин Д.С.) Oeritte: программное средство для объяснения контрпримеров для метода формальной верификации посредством проверки моделей // Сборник тезисов докладов конгресса молодых ученых. Электронное издание. – СПб: Университет ИТМО, [2020]. URL: https://kmu.itmo.ru/digests/article/4758