Le model checking borné (BMC) est une technique efficace de vérification formelle permettant de vérifier des propriétés souhaitées sur des exécutions bornées d’un modèle abstrait d’un système logiciel. Ces propriétés sont généralement décrites dans une logique temporelle, tandis que le système est modélisé comme un système de transitions d’états. Dans cet article, nous proposons une nouvelle logique de comptage, notée $\mathcal{L}{C}$LC, afin de décrire les propriétés temporelles des systèmes client-serveur comportant un nombre non borné de clients. Nous introduisons également une stratégie de model checking borné à deux dimensions ($2D$2D-BMC), qui utilise deux paramètres distincts : l’un pour le nombre d’étapes d’exécution, l’autre pour le nombre de jetons dans le réseau de Petri représentant le système client-serveur. Ces deux paramètres évoluent indépendamment, ce qui diffère des techniques classiques de BMC dans le cadre des réseaux de Petri. Cette stratégie $2D$2D-BMC est implémentée dans un outil nommé DCModelChecker, qui exploite la technique $2D$2D-BMC en conjonction avec un solveur de satisfiabilité modulo théories (SMT) de pointe, Z3. Le système est spécifié sous forme de réseau de Petri, et les propriétés exprimées dans $\mathcal{L}{C}$LC sont encodées en formules vérifiées par le solveur. Notre outil est également capable de traiter des benchmarks industriels provenant du Model Checking Contest (MCC). Nous présentons les résultats de ces expérimentations afin de démontrer la pertinence et l’efficacité de la stratégie $2D$2D-BMC.