Récemment, j'ai commencé à étudier les techniques de vérification formelles. Dans la littérature, vérificateur de modèle et solver sont utilisés d'une manière interchangeable. Mais, comment vérificateur de modèle et solveur sont connectés les uns aux autres?Solveur SMT/SAT vs Model Checker
p.s. J'apprécierais que certains documents ou liens soient suggérés.
Pour effectuer une vérification de modèle, une analyse d'accessibilité est nécessaire et, pour ce faire, les transitions de programme sont souvent exécutées symboliquement. La solution au problème de satisfaction résultant est créée par un solveur. Un très basique et très bonne introduction se trouve dans ce livre de texte libre (Partie III: Analyse et vérification):
Edward A. Lee et Sanjit A. Seshia, Introduction aux systèmes embarqués, une Cyber- Physical Systems Approach, deuxième édition, MIT Press, ISBN 978-0-262-53381-2, 2017
Pour la vérification des modèles, vous avez un modèle et une spécification (ou une propriété), et vous vérifiez si le modèle répond spécification.
En résolution SAT, vous avez une formule et vous essayez de trouver une affectation satisfaisante. Maintenant, dans la vérification de modèle, vous pouvez combiner le modèle et la négation de la propriété pour vous donner une formule. Utilisez un solveur pour résoudre cette formule. Si cela vous donne une solution, cela signifierait que la propriété est parfois violée (puisque vous avez conjugué la propriété niée). Obtenir unsat signifierait que votre modèle satisfait la propriété/spécification.