Systems and Means of Informatics
2022, Volume 32, Issue 2, pp 23-35
CONSTRUCTING OF THE BRIEF REACHABILITY TREE FOR PROGRAM MODELS IN TERMS OF PETRI NETS
- D. V. Leontyev
- D. I. Kharitonov
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.
[+] References (10)
- Leveson, N. G., and C. S. Turner. 1993. An investigation of the Therac-25 accidents. Computer 26(7): 18-41.
- Mako, S., M. Pilat, P. Svab, J. Kozuba, and M. Cicvakova. 2019. Evalutionof MCAS system. Acta Avionica J. 21(1):21-28.
- Kharitonov, D., and G. Tarasov. 2014. Modeling function calls in program control flow in terms of Petri nets. ACSIJ 3(6):82-91.
- Kharitonov, D. 2009. Razdel'naya verifikatsiya ob"ektno-orientirovannykhprogramm s postroeniem protokola C++ klassa v terminakh setey Petri [Separable object-oriented program verification with C++ class protocol definition in terms of Petri nets]. Modelirovanie i analiz informatsionnykh system [Modeling and Analysis of Information Systems] 16(1):92-112.
- Denaro, G., and M. Pezze. 2003. Petri nets and software engineering. DAIMI Report Series 29(1):439-466.
- Latvala, T., and M. Makela. 2004. LTL model checking for modular Petri nets. Applications and theory of Petri nets. Eds. J. Cortadella and W. Reisig. Lecture notes in computer science ser. Springer. 3099:298-311.
- Valmari, A. 1998. The state explosion problem. Lectures on Petri nets I: Basic models. Eds. W. Reisig and G. Rozenberg. Lecture notes in computer science ser. Springer. 1491:429-528.
- McMillan, K. L. 1993. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. Computer aided verification. Eds. G. von Bochmann and D. K. Probst. Berlin, Heidelberg: Springer. 164-177.
- Engelfriet, J. 1991. Branching processes of Petri nets. Acta Inform. 28(6):575-591.
- Kozyura, V.E. 2002. Realizatsiya sistemy proverki modeley raskrashennykh setey
Petri s ispol'zovaniem razvertok [Implementation of a system for checking models of colored Petri nets using developments]. Novosibirsk: A. P. Ershov IIS SB RAS. 44 p.
[+] About this article
Title
CONSTRUCTING OF THE BRIEF REACHABILITY TREE FOR PROGRAM MODELS IN TERMS OF PETRI NETS
Journal
Systems and Means of Informatics
Volume 32, Issue 2, pp 23-35
Cover Date
2022-06-10
DOI
10.14357/08696527220203
Print ISSN
0869-6527
Publisher
Institute of Informatics Problems, Russian Academy of Sciences
Additional Links
Key words
Petri nets; reachability tree; checking programs correctness; modeling program behavior
Authors
D. V. Leontyev  and D. I. Kharitonov
Author Affiliations
Institute of Automation and Control Processes, Far-Eastern Branch of the Russian Academy of Sciences, 5 Radio Str., Vladivostok 690041, Russian Federation
|