An Automatic HCPN Modeling Method for Microservice-Orchestrated Network Operation Workflows

Abstract

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.