ИАПУ ДВО РАН

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


2022

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

Article

Sistemy i Sredstva Informatiki | Systems and Means of Informatics

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

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