Parameterized systems play a crucial role in the computer field, and their security is of great significance. Formal verification of parameterized protocols is especially challenging due to its "parameterized" feature, which brings complexity and undecidability. Existing automated parameterized verification methods have limitations, such as facing difficulties in automatically deriving parameterized invariants constrained by mixed Forall and Exists quantifiers, or having challenges in completing the parameterized verification of large and complex protocols. This paper proposes a formal verification framework for parameterized systems based on induction, named wiseParaverifier. It starts from small concretizations of protocols, analyzes inductive counterexamples, and constructs counterexample formulas to guide the entire process of parameterized verification. It also presents a heuristic Generalize method to quickly find auxiliary invariants, a method for promoting complex mixed quantifiers and merging parameterized invariants, and uses symmetric reduction ideas to accelerate the verification process. Experimental results show that wiseParaverifier can successfully complete automatic inductive verification on 7 cache coherence protocols and 10 distributed protocols. It has strong verification capabilities and migration capabilities, and can provide concise and readable verification results, which is helpful for learners to understand protocol behaviors.

翻译：参数化系统在计算机领域扮演着至关重要的角色，其安全性具有重大意义。参数化协议的形式化验证因其"参数化"特性而尤为困难，该特性带来了复杂性和不可判定性。现有的自动化参数化验证方法存在局限性，例如在自动推导受全称量词与存在量词混合约束的参数化不变量时面临困难，或在完成大型复杂协议的参数化验证方面存在挑战。本文提出了一种基于归纳的参数化系统形式化验证框架，命名为wiseParaverifier。该框架从协议的小规模具体化实例出发，分析归纳反例，并构建反例公式以指导参数化验证的全过程。同时，本文提出了一种启发式的Generalize方法以快速寻找辅助不变量，一种用于提升复杂混合量词及合并参数化不变量的方法，并利用对称约简思想加速验证过程。实验结果表明，wiseParaverifier能够成功完成对7个缓存一致性协议和10个分布式协议的自动归纳验证。该工具具备强大的验证能力和迁移能力，并能提供简洁、可读的验证结果，有助于学习者理解协议行为。