有界模型检查（Bounded Model Checking, BMC）是一种高效的正式验证技术，可用于在系统抽象模型的有界执行路径上检验软件系统所期望的性质。这些性质通常以某种时序逻辑进行描述，而系统则被建模为状态转移系统。本文提出了一种新颖的计数逻辑 $\mathcal{L}{C}$LC，用于描述具有任意数量客户端的客户端-服务器系统的时序性质。此外，我们提出了一种二维有界模型检查（2D-BMC）策略，该策略引入两个可区分的参数：一个用于表示执行步数，另一个用于表示表示客户端-服务器系统的Petri网中的令牌数量。这两个参数在验证过程中独立演化，这与Petri网形式化框架下传统的BMC技术有本质区别。该2D-BMC策略已实现在名为DCModelChecker的工具中，该工具结合了先进的满足性模理论（Satisfiability Modulo Theories, SMT）求解器Z3，以实现高效的性质验证。系统以Petri网形式给出，而使用 $\mathcal{L}{C}$LC 描述的性质被编码为逻辑公式，交由SMT求解器进行检查。本工具还可应用于模型检查竞赛（Model Checking Contest, MCC）提供的工业级基准测试实例。我们通过实验结果展示了2D-BMC策略在实际应用中的有效性与可行性。