Microservice architecture, with distributed deployment and loose coupling, is widely used in networked service systems. As the number of service modules grows and cross-service interactions become complex, formal modeling and verification face challenges. Hierarchical Colored Petri Net (HCPN)-based model checking can verify full execution paths, but manual modeling is costly, error-prone, and prone to state-space explosion. This paper proposes an automated HCPN modeling method that transforms Netflix Conductor workflow specifications into hierarchical HCPN models using predefined rules. The method preserves workflow structure, control flow, and data dependencies, and generates models suitable for formal verification. Experimental results show that the generated HCPN models are consistent with the original workflows and can automatically detect errors such as data inconsistency and business-data state inconsistency. Compared with existing methods, this approach reduces manual effort, lowers modeling cost, and provides more comprehensive support for data representation and error detection.

STM32 microcontrollers contain multiple interrupt program types, and the occurrence and execution of various types of interrupts are uncertain, making it difficult to detect hidden vulnerabilities. Colored Petri Nets (CPN) can model the software system and find vulnerabilities in the program through model detection, but the uncertain triggering of the interrupt will lead to state explosion, and then the model detection cannot be completed, so this paper proposes an automatic modeling method to avoid state explosion for STM32 microcontrollers, which reduces the possibility of state explosion on the one hand, and improves the modeling efficiency on the other hand. Firstly, the program preprocessing is carried out, which is divided into two steps, one is to read, mark and classify and store the STM32 source program, and the other is to perform equivalent class division detection to find the correlation variables between programs to provide support for the subsequent combination model. Secondly, the coarse-grained modeling method proposed by the project team was used to classify and model the main program and interrupt program of STM32, and multiple or one source program sentence was described as a transition. Finally, different types of interrupt predefined model frameworks are designed, and based on the detection results of the previous equivalence class division, the constructed main program model fragments and interrupt model fragments are connected with the corresponding types of interrupt model frameworks at each data interaction point to form a complete model, and the equivalent substitution connects the interrupt model at all locations, so as to cover all interrupts that may lead to errors. In the experimental part, the correctness and effectiveness of the method are verified by an intelligent irrigation example.

For inductive link prediction in knowledge graphs, we address the problem by considering bridging links (i.e., links connecting discrete graphs). Although current research overcomes the traditional graph topological constraints, it tends to ignore the dynamic interactions between relations and entities as well as the capture of global information. The problem of discrete and small amounts of information in real-world knowledge graphs makes it difficult for existing methods to effectively integrate global and local information and to model complex relationships between entities. To address these issues, we propose a novel meta-analogy learning framework, Ank-motor, which integrates autonomously designed dynamic graph neural networks with analogical reasoning. The dynamic graph neural network models interactions and captures global information, while the analogical inference layer integrates entity, relation, and triple-layer information to capture local semantic details. In addition, meta-learning techniques are utilized to deal with problems with small amounts of data and to enhance the model’s ability to generalize to new tasks. Numerous experiments show that Ank-motor significantly outperforms existing models on multiple benchmark datasets.

In the formal modeling and verification of trusted concurrent systems (such as distributed trusted computing platforms and secure communication protocols), the complex inter-leaving of behaviors easily triggers state space explosion, greatly reducing the efficiency of model checking. Although Colored Petri Nets (CPNs) can effectively represent concurrent behaviors and data interactions, their models often contain a large number of redundant structures irrelevant to the properties to be verified, thereby impairing the efficiency of verifying the core properties of trusted systems. This paper proposes a CPN model reduction method based on Unrelated Transitions—transitions in the model that have no data relationship with the properties to be verified. By identifying and eliminating behaviors irrelevant to the properties to be verified, the method achieves efficient state space reduction while ensuring the consistency of property verification results, thus providing technical support for the verification of trusted systems. Specifically, through data-flow analysis of property formulas, Unrelated Transitions with no data interaction with the target properties are identified. Then, all behaviors of the reduced model elements are integrated into adjacent model components. On the premise of preserving the model behaviors and their relationships (such as sequence, choice, and concurrency) unchanged, operations including arc expression encapsulation, conditional transfer, and arc redirection are employed to reduce the number of irrelevant nodes while ensuring the model remains connected and executable. Experimental results show that the state space of the reduced model is significantly compressed, and the verification results of the properties to be verified remain completely consistent before and after reduction, which demonstrates the effectiveness and correctness of the proposed method in improving the efficiency of modeling and verification for trusted systems.

Colored Petri nets (CPNs) provide descriptions of the concurrent behaviors for software and hardware. Model checking based on CPNs is an effective method to simulate and verify the concurrent behavior in system design. However, the model-checking method traverses the full state space, which suffers from the state-space explosion problem. A reduced state-space generation method related to the property of concurrent systems is proposed. Specifically, we extend CPNs to define a property-related model (CPN-PR) and give a property-related analysis method whose results can be used to generate the CPN-PR model. A reduced state-space generation method is developed based on enabled binding element filtering rules. The stutter trace equivalence between the state spaces of CPN and CPN-PR has been proven by showing that the reduced state space may not change the model-checking result. A comparison experiment is conducted to demonstrate the effectiveness of our method.

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.

Model checking is a formal method used to verify the correctness of hardware or software system designs and implementations. This kind of algorithm typically involves exhaustively searching the system’s state space to determine if the property is satisfied. Colored Petri Nets (CPN) is a graphical language for building system models and analyzing their properties, which can accurately describe concurrent behavior in software and is suitable for describing complex concurrent systems. At present, some studies extend Computational Tree Logic (CTL) on CPN, but Linear Temporal Logic (LTL) does not, and there are still shortcomings in transition property verification. LTL needs to be combined with the state information and transition firing information of CPN to achieve the model compatible property description. Therefore, this paper proposes an ASK-LTL model detector: ASK-LTL temporal logic is proposed, which is an extension of LTL, and can consider both state information and transition information. The model checking algorithm is proposed. First, simplify the ASK-LTL formula and convert it into a ASK-LTL Büchi automaton (ALGBA). Second, perform calculations using the automaton and CPN state space to generate a product automaton. Third, look for complete paths in the product automaton. This method not only retains the characteristics of LTL, but also can detect the transition information in CPN model. Finally, the correctness and effectiveness of the method are verified by the experiment of vending machine.

Time-triggered (TT) network provides a low-cost service to meet the strong demand of modern industry networks for real-time communication. Both simulation and reachability analysis provide effective research methods for TT networks. This paper presents a verification framework for the TT network based on Timed Colored Petri Nets (TCPN). We propose an automatic formal modeling method for the behavior of message transmissions in the TT network. We harness timed multisets of TCPN to model and analyze time-triggered message transmission latencies. For a holistic system evaluation, we characterize the critical system properties such as boundedness and liveness. We substantiate the properties by the reachability analysis. We demonstrate the effectiveness through a case study by simulating the message transmission and reachability analysis in the state space. Finally, we analyze the influencing factors of the state space in the automotive scenario. The proposed automatic modeling method can effectively reduce the state space scale.

Abstract The state space explosion restricts the error detection of concurrent software. The abstraction can provide a solution to avoid state space explosion, but it is easy to ignore important details, resulting in inaccurate detection results. This paper proposes a methodology of fine‐coarse‐grained automatic modelling for Java source programs. By the principle that the execution details of property‐unchecked, non‐interactive, and unrelated statements do not affect the model checking results, we model coarse‐grained model fragments for such statements, while fine‐grained model fragments for property‐checked, interactive, and related statements. Our method reduces the model and state space and ensures the error detection of the source program based on model checking. Moreover, we prove the equivalence of the fine‐grained model, the coarse‐grained model, and the program. Finally, this paper gives an experiment to verify the effectiveness of the proposed method.

In order to solve the state explosion problem that makes model checking difficult to perform, this paper proposes a state space pruning algorithm. The property transition set is extracted from the ASK-CTL formula and the irrelevant transition set, which represents behaviors independent of the property to be detected is obtained through the data dependence relationship. To simplify the state space, the algorithm reduces concurrent occurrences of irrelevant transitions, which does not change property checking. The experimental results show that the state space pruning algorithm reduces the number of states and arcs of the state space, and improves the verification efficiency.

Modeling and testing for parallel software systems is difficult, because the number of states and execution fragments expand significantly caused by parallel behaviors, so that many traditional testing methods cannot work effectively for this kind of software. In this paper, a test sequence generation method based on model reduction for parallel software systems is shown. Firstly, a formal model for software system specification is constructed based on Coloured Petri Net (CPN), called system model; and a model reduction method based on trace-equivalent principle is shown and applied on system model, which could generate an external behavior equivalent model with smaller scale. Secondly, a linear behavior sequence of the system is specified using CPN, called LBS model, which represents testing purpose in a test case, and some operations between state space diagrams of system model and LBS model are defined, so that a sub-graph of system model state space diagram is generated, which could cover all executions of system model that involves behaviors of LBS. Finally, a performance analysis shows the effectiveness of the method.