Bounded model checking (BMC) is an efficient formal verification technique which allows for desired properties of a software system to be checked on bounded runs of an abstract model of the system. The properties are frequently described in some temporal logic and the system is modeled as a state transition system. In this paper we propose a novel counting logic, $\mathcal{L}_{C}$, to describe the temporal properties of client-server systems with an unbounded number of clients. We also propose two dimensional bounded model checking ($2D$-BMC) strategy that uses two distinguishable parameters, one for execution steps and another for the number of tokens in the net representing a client-server system, and these two evolve separately, which is different from the standard BMC techniques in the Petri Nets formalism. This $2D$-BMC strategy is implemented in a tool called DCModelChecker which leverages the $2D$-BMC technique with a state-of-the-art satisfiability modulo theories (SMT) solver Z3. The system is given as a Petri Net and properties specified using $\mathcal{L}_{C}$ are encoded into formulas that are checked by the solver. Our tool can also work on industrial benchmarks from the Model Checking Contest (MCC). We report on these experiments to illustrate the applicability of the $2D$-BMC strategy.

翻译：有界模型检测（BMC）是一种高效的形式化验证技术，它允许在系统抽象模型的有界运行上检查软件系统的期望属性。这些属性通常用时态逻辑描述，系统则建模为状态转移系统。本文提出了一种新颖的计数逻辑 $\mathcal{L}_{C}$，用于描述具有无界数量客户的客户-服务器系统的时态属性。我们还提出了二维有界模型检测（$2D$-BMC）策略，该策略使用两个可区分的参数：一个用于执行步数，另一个用于表示客户-服务器系统的网中的令牌数量，且这两个参数独立演化，这与Petri网形式化中的标准BMC技术不同。该$2D$-BMC策略在名为DCModelChecker的工具中实现，该工具结合了$2D$-BMC技术与先进的可满足性模理论（SMT）求解器Z3。系统以Petri网形式给出，使用$\mathcal{L}_{C}$指定的属性被编码为由求解器检查的公式。我们的工具也能处理来自模型检测竞赛（MCC）的工业基准测试。我们报告了这些实验以说明$2D$-BMC策略的适用性。