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.

Collaborative systems involve a significant amount of concurrent behaviors, which makes the verification of system reliability challenging. Colored Petri Nets are suitable for concurrent description and supports model checking, contributing to improving the quality of collaborative systems. However, there is the problem of state space explosion leading to difficult completion of model checking. This paper automates the simplification of the model by abstracting the data in the model that are irrelevant to the property formulas and removing the corresponding data processing and irrelevant behaviors. The method first performs correlation analysis of the variables in the model based on the property formula, and then deletes the corresponding data (i.e., token) and color set type by the obtained set of irrelevant variables. In addition, model descriptions corresponding to irrelevant data processing are also removed. The deletion of these places, transitions and directed arcs, reduces the number of concurrent behaviors, thus achieving the goal of scaling down the model and its state space. Finally, the effectiveness and correctness of the method were verified through experiments.

The performance of parallel programs is affected by load balancing, inter-thread communication and scalability, etc. Timed Colored Petri Net(TCPN) enables efficient modeling of Java parallel source programs to implement performance analysis. However, constructing a TCPN model that is consistent with the source code is difficult, and accurate performance analysis relies on time information in the model. This paper gives a time determination strategy and proposes an automatic generation method for the TCPN model. We determine the time delay based on the time complexity of the code segment corresponding to the transition or output arc combined with the actual running time of the common operations. Experiments have verified that the method can automatically generate valid TCPN models, helping developers to easily analyze performance bottlenecks.