Rendre la vérification des bogues dans la conception de logiciels et de matériel moins chère et plus efficace

Logiciel

Crédit : domaine public CC0

Le développement de matériel et de logiciels complexes est source d’erreurs et coûteux. Les tests peuvent détecter la présence de bogues dans ces conceptions, mais ils ne peuvent pas prouver leur absence. Une technique qui peut fournir des informations utiles sur l’exactitude des conceptions de systèmes est la vérification des modèles. La vérification des modèles est une technique de raisonnement automatisé pour trouver des failles dans les systèmes matériels et logiciels. doctorat Le candidat Muhammad Mahmoud a repensé les algorithmes pour les rendre plus adaptés à la vérification de modèles à l’aide de GPU, qui permettent un calcul parallèle à faible coût.

La vérification des modèles est utilisée pour détecter les bogues potentiels le plus tôt possible, de préférence lors de la phase de conception, afin d’apporter les modifications nécessaires rapidement et à moindre coût. Des exemples réussis de vérification de modèles incluent la vérification des contrôleurs du CERN, des enclenchements ferroviaires, des systèmes de contrôle nucléaire et de l’imagerie médicale. Des entreprises telles qu’Amazon, Microsoft et Facebook utilisent et développent une technologie de vérification des modèles pour s’assurer que leurs produits se comportent de manière fonctionnelle.

Vérification de modèle borné

Cependant, la vérification de modèle est très exigeante en termes de calcul. Il s’agit d’analyser de manière exhaustive la conception d’un système pour déterminer s’il satisfait aux spécifications fonctionnelles souhaitables.

Le Bounded Model Checking (BMC) est une technique symbolique contemporaine qui permet d’analyser de grandes conceptions en un temps raisonnable. BMC détermine si un modèle satisfait une certaine propriété exprimée en logique temporelle, en traduisant le problème de vérification de modèle en un problème de satisfiabilité propositionnelle (SAT), par exemple.

Dans cette thèse, Muhammad Mahmoud, du groupe de recherche Génie logiciel et technologie du département de mathématiques et d’informatique, a étudié comment les unités de traitement graphique (GPU) peuvent être utilisées efficacement pour BMC, en se concentrant sur le raisonnement sur SAT. Les GPU offrent un grand potentiel pour le calcul parallèle, tout en maintenant une faible consommation d’énergie.

Cependant, tous les types de calcul ne peuvent pas être trivialement exécutés sur des GPU, dans la plupart des applications, les algorithmes doivent être entièrement repensés.

Simplifier les formules

Le chercheur s’est concentré sur les simplifications des formules SAT, une stratégie qui conduit à une réduction drastique de la taille de la formule et de l’espace de recherche.

Ensuite, il a présenté un nouveau solveur SAT qui entrelace rigoureusement la recherche avec ce que l’on appelle l’inprocessing. L’inprocessing s’est avéré puissant dans les solveurs SAT modernes, en particulier lorsqu’il est appliqué sur des formules SAT encodant des problèmes de vérification logicielle et matérielle.

Le nouveau solveur est hybride, capable d’exécuter la partie parallèle sur le GPU tandis que la résolution proprement dite s’exécutera séquentiellement sur l’unité centrale de traitement (CPU).

Dans sa thèse, Mahmoud aborde également les aspects de conception des structures de données et la gestion de la mémoire de nos implémentations parallèles, conduisant à des améliorations substantielles des performances d’exécution.

Prise de décision multiple

Concernant la partie résolution, il a étendu l’algorithme de recherche Conflict-Driven Clause Learning (CDCL) à la prise de décision multiple (MDM).

La procédure MDM a la capacité de prendre et de propager plusieurs décisions à la fois. De plus, il est complété par une recherche locale pour améliorer la précision de l’attribution de valeurs de vérité à ces décisions.

Enfin, il a intégré le solveur à un vérificateur de modèle borné de pointe. Après avoir optimisé davantage le moteur de traitement et rendu le processus de résolution incrémentiel, il a étudié l’impact du BMC compatible GPU sur la vérification logicielle à l’aide de la bibliothèque Amazon Web Services (AWS) C99.


Vérification intelligente des bogues pour les logiciels


Plus d’information:
Raisonnement automatisé activé par GPU. research.tue.nl/files/19516561 … 0310_Muhammad_hf.pdf

Fourni par l’Université de technologie d’Eindhoven

Citation: Rendre la vérification des bogues dans la conception logicielle et matérielle moins chère et plus efficace (15 mars 2022) récupéré le 15 mars 2022 sur https://techxplore.com/news/2022-03-bug-checking-software-hardware-cheaper-efficient .html

Ce document est soumis au droit d’auteur. En dehors de toute utilisation loyale à des fins d’étude ou de recherche privée, aucune partie ne peut être reproduite sans l’autorisation écrite. Le contenu est fourni seulement pour information.