Верификация в АНИС

Выполнение верификации

На данном этапе проделаны следующие шаги:

• написана формальная модель

• формальная модель готова для динамической верификации (подобраны значения констант и несущих множеств)

• указан адаптер монитора и формат трасс

• трассы загружены

• разработан и реализован медиатор

• рабочая среда настроена, все необходимые компоненты установлены и сконфигурированы

Тем самым, все готово для выполнения динамической верификации. Нужно перейти на вкладку Testing и выполнять отображаемые там тесты.

Средства тестирования VSCode позволяют фильтровать показываемую часть тестов и, впоследствии, запускать лишь часть тестов.

Отладка

Среда содержит средства отладки, чтобы разобраться с тестами, которые не проходят.

Первым делом тест, который не проходит, нужно запустить в режиме отладки. Для этого нужно на вкладке Testing найти нужный тест (помечен красной иконкой) и справа от него нажать на значок отладки. Если средства отладки до этого не использовались, выполнение в режиме отладки завершится без остановки на месте возникновения исключительной ситуации. Чтобы оно остановилось, нужно перейти на вкладку Run and Debug и в разделе Breakpoints нажать Uncaught Exceptions. Перезапускаем тест в режиме отладки и теперь он должен остановиться. Далее можно продолжить выполнение пошагово, использовать Debug console, просматривать значения текущих переменных на вкладке Run and Debug, просматривать там же стек вызовов.

Если исключительная ситуация генерируется внутри служебного кода АНИС, отладка может быть затруднена. АНИС пытается частично в этом помочь. А именно, если необходимо упростить отладку выполнения модельной трассы на модели, можно запустить отладку с генерацией отладочных модулей. Это такие python-модули, которые тоже проверяют модельную трассу на модели, но выглядят проще за счет меньшего использования служебного кода АНИС. Для включения этого режима нужно открыть Settings, найти настройку Make Debug Modules и поставить галочку.