Research on Java Automatic Simplified Modeling Based on Source Code Dependency Analysis
Jiaqi Wang, Tao Sun, Wenjie Zhong, Ziyu Wang, Yefan Zhang · 2024
Program model checking is an effective technique for ensuring the reliability of software systems. In collaborative systems, the presence of the state space explosion poses difficulties for model checking. In the program, the values of variables represent the program’s state. The property formula focuses on the values of certain variables, which are referred to as key variables. Other variables in the program may or may not affect these key variables; those that do are called relevant variables. By analyzing and detecting relevant variables, simplifying unrelated variables, the reduction modeling is completed. This paper proposes a Java automatic simplified modeling method based on source code dependency analysis. Firstly, some information of the source program is removed during the program analysis phase based on the results of dependency analysis. Then, constructs a Colored Petri Net model from the reduced code during the modelling phase. In this process, only the code relevant to the target key variables associated with the properties under consideration is retained for model description. Without affecting the property check results, reduce the size of the model and state space; the reduced model contains property-related codes that are consistent with the source program. The method automatically generates a smaller model, alleviates the state space explosion and improves the model checking efficiency. Finally, we use a practical example to verify the method’s effectiveness.