AI 中文总结
针对模型检查的状态空间爆炸问题，提出结合模型检查与仿真关系的技术，以简单通信协议、交替比特协议和滑动窗口协议为研究对象，通过在较小状态机上模型检查及仿真关系组合，实现对大可达状态空间协议的形式化验证。
AI 中文摘要
模型检查是验证系统或协议属性的强大技术，但常面临状态空间爆炸问题。对于交替比特协议（ABP）和滑动窗口协议（SWP）等协议，增加参数会使可达状态空间过大，无法进行穷举模型检查。为此，我们提出一种将模型检查与仿真关系相结合的技术。重点关注简单通信协议（SCP）、ABP和SWP这三个协议，它们按抽象程度递减呈现，可达状态相应增加。SCP可直接模型检查，ABP和SWP参数增加时直接模型检查不可行。我们通过结合SCP的模型检查与ABP到SCP的仿真关系证明ABP满足不变性属性，通过SWP到ABP和ABP到SCP的仿真关系组合及SCP的模型检查证明SWP满足不变性属性。这些方法通过在小得多的状态机上进行模型检查实现对大可达状态空间协议的形式化验证。
英文摘要
Model checking is a powerful technique for verifying properties of systems or protocols, but it often suffers from the state space explosion problem. For protocols such as the Alternating Bit Protocol (ABP) and the Sliding Window Protocol (SWP), increasing parameters such as channel capacities or window sizes leads to a reachable state space that is infeasible for exhaustive model checking. To address this, we propose a technique that combines model checking with simulation relations. We focus on three protocols: the Simple Communication Protocol (SCP), ABP, and SWP. Formalized as state machines, these protocols are presented in decreasing order of abstraction: SCP, ABP, and then SWP, which results in a corresponding increase in reachable states. While SCP is verifiable through direct model checking without state space explosion, the direct application of model checking to ABP and SWP becomes infeasible as their parameter values increase. We demonstrate that ABP satisfies its invariant property by combining model checking on SCP with a simulation relation from ABP to SCP. Furthermore, we demonstrate that SWP satisfies its invariant property through the composition of simulation relations from SWP to ABP and from ABP to SCP, in conjunction with model checking on SCP. These approaches enable the formal verification of protocols with large reachable state spaces by conducting model checking on a significantly smaller state machine.
