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

D. V. Leontyev, D. I. Kharitonov

Institute of Automation and Control Processes, Far-Eastern Branch of the Russian Academy of Sciences, 5 Radio Str., Vladivostok 690041, Russian Federation

Abstract: The article deals with the problem of building a state space for analyzing the imperative programs behavior. The state explosion problem of analyzed states number in the automatic program models construction is the main problem for finding errors in the programs source code. This explosion is induced mainly due to the composition of the program variables states. The article proposes an approach to reducing the number of states of the reachability tree of program models by separating the program control flow model from the variable models and then adding only variables that affect the control flow and reducing the states of these variables. The example considered in the article shows how such an approach can be applied in practice.

Keywords: Petri nets, reachability tree, checking programs correctness, modeling program behavior.

Received: 30.11.2021

DOI: 10.14357/08696527220203