Outil de vérification de modèle simple

Question

Existe-t-il un outil simple de vérification de modèle? Je prévois de mettre en œuvre un outil de vérification de modèle qui analysera le code pour certaines des propriétés prédéfinies.

Answer 1

Un des outils importants est SPIN , avec le langage Promela. Si vous utilisez LaTeX, il existe également un TLA + .

Celles-ci n’analyseront pas votre code, mais vous permettront d’exprimer un modèle pour vos hypothèses et vos transitons d’états, puis d’analyser les états non valides. En d’autres termes, ils détecteront les problèmes de votre modèle, pas la mise en œuvre de votre modèle.

J'ai vu une démonstration de Goanna , mais je ne le fais pas. t pas savoir si elle est disponible (commerciale ou autre); cela a l’avantage d’analyser votre code source.

En regardant simplement votre question, et les commentaires dans votre question à nouveau, il semble que vous devriez vraiment lire une partie de la littérature en premier. Peut-être, l'outil de vérification du modèle de rotation , ou Spécification des systèmes (téléchargeable à partir de Site Web de Leslie Lamport ). Vous devez reformuler votre problème afin de ne pas essayer de résoudre le problème persistant.

Answer 2

CBMC est un outil simple, à ma connaissance. fonctionne réellement sur le code. La vérification de modèle en général est un domaine qui a fait l'objet de nombreuses recherches, mais comme l'ont déjà souligné d'autres personnes, il est difficile de suggérer quelque chose avec les informations fournies. Il existe des milliers de solveurs SAT, des outils formels de vérification HDL / machine à états et de nombreux analyseurs de sources statiques du commerce.

Dans tous les cas, la CBMC est un bon outil, mais ne me croyez pas sur parole. Ed Clarke, le principal membre du corps professoral à l'origine de ce travail, a remporté le prix Turing cette année ;-)