ИАПУ ДВО РАН

Constructing of the brief reachability tree for program models in terms of Petri nets


2022

Kharitonov D. I., Leontiev D. V.

Системы и средства информатики

Article

Sistemy i Sredstva Informatiki | Systems and Means of Informatics

Federal Research Center Computer Science and Control of the Russian Academy of Sciences

23-35

Leontyev D.V., Kharitonov D.I. Constructing of the brief reachability tree for program models in terms of Petri nets // Systems and Means of Informatics. 2022. Vol. 32, no 2. Pp. 23-35. https://doi.org/10.14357/08696527220203. (in Russian).

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

10.14357/08696527220203

http://mi.mathnet.ru/ssi824