Concurrent Software Fine-Coarse-Grained Automatic Modeling Method for Algorithm Error Detection

摘要

Concurrent software state space explodes, which makes algorithm error detection difficult. This paper proposes a fine-coarse-grained automatic modeling method. Based on the JAVA concurrent program, we generate the HCPN (Hierarchical Coloured Petri Net) fine-coarse-grained model that in accordance with the behavior of the source program automatically. The goal is to detect the algorithm errors in the program through the model checking technology. We complete the modeling of interactive, property-related and specific structure statements through fine-grained method and complete the modeling of other statements through coarse-grained method. Avoid the state space explosion effectively under the premise of retaining the interaction behavior and the property-related behavior execution path. This paper verifies the effect of fine-coarse-grained automatic modeling method by comparing and analyzing the experimental results.