DCA2MC découpe le model checking et réduit la mémoire

Dans le schéma de l’équipe, un vaste problème de vérification commence par un état initial et se déploie en un espace d’états accessibles. DCA2MC, développé par le professeur Kazuhiro Ogata, le professeur associé Tsubasa Takagi et le maître de conférences Canh Minh Do à l’Institut supérieur des sciences et technologies de Nara au Japon, découpe cet espace en couches et vérifie indépendamment les éléments plus petits.

Le model checking est une méthode automatisée permettant de vérifier qu’un système matériel ou logiciel respecte des exigences définies. Son principal obstacle est l’explosion de l’espace des états : à mesure que les systèmes se complexifient, le nombre d’états à examiner peut rendre la vérification directe trop exigeante en mémoire ou en temps. DCA2MC s’attaque à ce goulot d’étranglement pour les propriétés temporelles linéaires, c’est-à-dire les exigences concernant le comportement d’un système au fil du temps, en utilisant une stratégie de type diviser pour régner.

Les chercheurs ont développé l’outil dans Maude, un langage fondé sur la logique de réécriture. Il peut traiter les sous-problèmes séquentiellement ou en parallèle, ce qui permet aux vérifications indépendantes d’exploiter les ressources de calcul multicœurs. Il peut également se connecter à des vérificateurs de modèles externes, dont Spin, sans nécessiter de modification de leurs algorithmes sous-jacents. Dans des études de cas portant sur cinq protocoles d’exclusion mutuelle, DCA2MC a mené à bien plusieurs tâches de vérification que d’autres outils ne pouvaient pas terminer avec la mémoire disponible, tout en prenant nettement moins de temps que le vérificateur de modèles LTL de Maude dans plusieurs cas.

Concrètement, alors ? Les ingénieurs et les chercheurs pourraient tenter de vérifier des systèmes numériques plus grands avant de simplifier l’analyse ou d’y renoncer en raison des limites matérielles. Les bénéficiaires potentiels incluent les développeurs travaillant sur des véhicules autonomes, des systèmes numériques et des systèmes de contrôle industriels, mais l’étude rend compte d’expériences plutôt que d’un déploiement dans ces environnements. Un système de commande semi-automatisé aide également les utilisateurs à choisir les configurations de couches, réduisant le recours aux essais et erreurs pour équilibrer l’utilisation de la mémoire et le temps d’exécution.

Le résultat est un outil et une méthode au stade de la recherche, et non la preuve que tous les grands systèmes peuvent désormais être vérifiés automatiquement. Les performances dépendent du choix de profondeurs de couches adaptées, et les comparaisons rapportées portent sur les cinq études de cas consacrées aux protocoles. Les résultats de l’équipe ont été publiés dans ACM Transactions on Software Engineering and Methodology le 31 juillet 2026.