Details

Данная работа посвящена созданию инструмента, генерирующего модель заданной Kotlin-программы на языке nuXmv для её последующей верификации с помощью инструмента проверки модели. Также для удобства применения нового инструмента на практике, он был интегрирован в среду разработки IntelliJ IDEA в виде плагина. В ходе выполнения работы были рассмотрены существующие инструменты проверки модели, предложен подход к автоматизации анализа корректности программ, а также создан и протестирован плагин, позволяющий автоматизировать верификацию заданной Kotlin-программы с применением метода проверки модели. Разработанный подход к автоматизации анализа корректности программ подразумевает использование специальных аннотаций, позволяющих в том числе помечать автоматные переменные, а также промежуточного представления Jimple (библиотека SootUp) для анализа исследуемого алгоритма. В результате был разработан инструмент, упрощающий процесс поиска ошибок в логике работы алгоритма программы, применение которого позволяет повысить качество создаваемых продуктов.

The given work is devoted to the creation of a tool that generates a model of a given Kotlin program in the nuXmv language for its subsequent verification using the model checking tool. Also, for the convenience of using the new tool in practice, it has been integrated into the IntelliJ IDEA development environment as a plug-in. In the course of the work, existing model verification tools were reviewed, an approach to automating program correctness analysis was proposed, and a plugin was created and tested that allows automating verification of a given Kotlin program using model checking. The developed approach to automating the analysis of the correctness of programs involves the use of special annotations, which allow, among other things, marking automatic variables, as well as an intermediate representation of Jimple (the SootUp library) for analyzing the algorithm under study. As a result, a tool has been developed that simplifies the process of finding errors in the logic of the program algorithm, the use of which allows you to improve the quality of the products being created.