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.
Guoshuai Li, Tao Sun, Wenjie Zhong· Proceedings of the ACM SIGCO...· 0 citations
Neural network repair aims to correct prediction failures caused by multiple security threats—such as backdoor attacks, natural corruptions, and safety property violations—through limited adjustments to model parameters. However, most existing repair methods rely on single-sample, point-to-point correction strategies, overlooking the statistical regularities of the feature space. As a result, they are highly sensitive to the scale of faulty samples and struggle to simultaneously achieve repair generalization and original performance preservation under small-sample settings. To address these limitations, we propose a novel general neural network repair paradigm termed NCCDA (Neuron-wise Class-Conditional Distribution Alignment). The method is grounded in a key insight: prediction failures fundamentally arise from neuron-level internal representations deviating from the high-likelihood regions corresponding to their true classes. NCCDA constructs neuron-wise class-conditional distribution references and formulates the repair process as a joint optimization of distribution alignment and structure preservation. By guiding abnormal representations back to high-likelihood regions while anchoring the structure of normal samples, the method enables efficient and adaptive repair without explicit neuron localization. We theoretically prove a generalization error bound under small-sample settings based on Rademacher complexity, providing formal guarantees. Extensive experiments across 7 benchmark datasets and 38 models, covering three categories of repair tasks, demonstrate that NCCDA consistently outperforms existing methods in repair effectiveness, generalization repair capability (Gene), and original accuracy preservation.
Liming Bao, Yan Wang, Tao Sun· Proceedings of the 32nd ACM...· 0 citations
