La vérification des machines à états finis (FSM) semble intimidante non pas parce que les FSM sont intrinsèquement ingérables, mais parce que la méthode de vérification devient opaque. Ce qu’il faut rendre à nouveau maîtrisable, c’est le travail de vérification lui-même : ce qui a été testé, ce qui reste en dehors de ce comportement testé, et comment les modifications affectent le chemin vers la couverture. Rendre la FSM explicite sous forme de graphe rétablit la structure visible nécessaire pour mener ce travail en s’appuyant sur une base de jugement plus solide.
La vérification des automates finis (FSM) semble intimidante principalement parce que la méthode est opaque, et non parce que les automates finis sont impossibles à gérer.
La vérification des automates finis (FSM) n’a pas besoin d’être intimidante. Pourtant, dans de nombreux projets, l’automate fini se perd dans des instructions « case » imbriquées, des séquences locales empilées et des appels de séquences obscurs. La tâche devient encore plus ardue lorsque plusieurs automates finis sont imbriqués les uns dans les autres ou interagissent pour produire un comportement plus large. Ce qui devrait rester un comportement structuré à vérifier devient une implémentation dispersée qu’il faut déchiffrer, étendre et réparer. C’est ce qui rend la tâche intimidante. La méthode elle-même devient opaque, la structure de la machine à états finis échappe à la vue. Et même les petites mises à jour commencent à paraître irréalisables car leur impact réel devient difficile à percevoir.
Lorsque le comportement couvert est opaque, la confiance s’effrite avant même que les plannings ne soient remis en cause.
Le véritable préjudice causé par l’opacité réside dans le fait que la vérification devient difficile à mener à bien et pénible à adapter lorsque la conception évolue. Un projet peut accumuler des tests, des régressions et des variantes de séquence, tout en ayant encore du mal à montrer quelles parties du comportement prévu du FSM ont réellement été testées et lesquelles restent inexplorées. La clôture cesse alors d’être un objectif technique clair et devient une cible mouvante.
Cette même opacité rend le changement coûteux. Lorsqu’un état, une transition ou un cas limite évolue, l’impact de cette mise à jour est difficile à retracer dans un code dispersé, de sorte que même une petite modification peut déclencher une refonte importante et fragile. Une fois que la clôture devient incertaine et que le changement devient coûteux, la seule véritable voie à suivre consiste à rétablir une structure visible pour le comportement en cours de vérification.
Rendez le FSM explicite à partir de la spécification, et l’essentiel du travail sera déjà fait.
Pour sortir de l’opacité, il faut rendre le FSM explicite. Si le comportement prévu est reconstitué à partir de la spécification sous forme de graphe, le vérificateur ne part plus d’un code dispersé, mais d’une structure visible qui peut être examinée, discutée et remise en question directement. Les états et les transitions sont identifiés d’emblée au lieu de rester cachés au sein du banc de test. Ils forment le FSM destiné à être testé par le travail de vérification. Cela élimine déjà la partie la plus difficile du travail : rendre le comportement prévu suffisamment explicite pour qu’il puisse être examiné, discuté et considéré comme fiable en tant que structure commune. Une fois cette structure explicite, le reste de la méthode dispose d’une base solide pour l’automatisation et l’exécution, au lieu d’être reconstruit à la main.
Lorsque la méthode est visible, la confiance revient.
Un comportement testé et visible rend la vérification plus fiable. Une fois que le FSM est représenté explicitement sous forme de graphe, le comportement testé n’a plus besoin d’être déduit à partir de tests de régression, de vérifications ponctuelles ou de l’activité de séquences locales. Il peut être examiné à la lumière d’une structure accessible à tous : le graphe. Ce qui a été testé, ce qui reste en dehors de ce comportement testé et les endroits où un changement aura un impact réel deviennent tous plus faciles à identifier et à discuter. Cela donne au vérificateur une base de jugement plus solide. Cela renforce également la confiance dans l’automatisation, car celle-ci agit désormais sur une structure déjà comprise.
Le graphe devient la vérification.
Le graphe devient la structure à partir de laquelle la vérification s’effectue. Une fois que l’automate fini (FSM) est explicité sous forme de graphe, la vérification n’a plus besoin de reconstituer le comportement prévu à partir d’un code dispersé.Elle peut suivre le comportement sous la même forme visible qui le définit. Les états contiennent alors les vérifications attendues, les transitions assurent le déplacement à travers l’automate fini, et randsequence pilote cette exploration ordonnée à travers le graphe. À partir de cette structure, la méthode peut produire les fonctions à implémenter. Le vérificateur peut alors se concentrer sur le contenu de ces fonctions plutôt que sur la reconstruction du flux de la vérification elle-même. Suivre le graphe est la bonne manière pour la vérification d’exercer l’automate fini que le graphe rend déjà explicite.
Une fois la vérification effectuée à partir de ce graphe, les comportements testés et non testés redeviennent distinguables. C’est ce qui rétablit la couverture, car la méthode peut désormais montrer ce qui a été exploré et ce qui reste en dehors des comportements testés. La couverture des états et des transitions peut alors être mesurée directement sur ce même graphe. Et randsequence peut continuer à orienter l’exploration vers les parties qui restent non couvertes. La clôture de couverture s’intègre au cœur de la méthode au lieu de rester un rapport généré en parallèle. Elle devient la preuve visible, au sein même de la méthode, que le comportement de l’automate fini représenté par le graphe a bel et bien été testé.
La méthode réduit l’opacité, mais la rigueur reste essentielle.
La méthode ne décharge pas le vérificateur de sa tâche de vérification. Elle peut rendre le comportement visible, organiser l’exploration, réintégrer la couverture dans le travail, et même structurer les fonctions à implémenter. Mais elle ne décide pas de ce que le graphe doit contenir, de quel comportement importe, ni de ce qui constitue un contrôle valide. Ces choix restent du ressort du vérificateur. La méthode réduit l’opacité, mais elle ne supprime pas la responsabilité.
La visibilité, la confiance et la couverture obtenues grâce à cette méthode ne restent valables que dans des conditions appropriées. Le graphe, le comportement attendu et les vérifications associées à ce comportement peuvent tout de même être erronés. Si tel est le cas, une structure explicite, voire une fermeture complète, ne fera que renforcer davantage cette interprétation erronée. La méthode rend la vérification visible et opérationnelle, mais elle ne détermine pas si le comportement modélisé est solide ou correct. La solidité et la correction dépendent toujours du vérificateur.
La méthode fait déjà avancer le travail de manière décisive pour un seul automate fini (FSM). En contrepartie, elle montre que les automates finis ne sont pas la véritable source du problème. Le plus difficile consiste à définir l’automate fini adapté au comportement que la conception met réellement en œuvre. Lorsque ce comportement émerge d’automates finis imbriqués ou de l’interaction entre plusieurs automates finis, la réalité modélisée dépasse le cadre d’une machine isolée. Utiliser correctement la méthode au niveau des automates finis imbriqués et en interaction devient alors l’art d’exprimer correctement le comportement global approprié.
Choisissez l’étape suivante qui correspond à vos besoins actuels.
La prochaine étape dépend des besoins actuels de votre travail de vérification. Si vous souhaitez appliquer directement la méthodologie, celle-ci est disponible via l’outil uGRASP et son livre blanc. Si le comportement à modéliser dépasse le cadre d’un seul automate fini (FSM) pour inclure des automates finis intégrés ou en interaction, la méthode doit être utilisée à ce niveau supérieur. C’est là qu’AEDVICES peut vous aider dans le travail de modélisation nécessaire pour exprimer correctement ce comportement plus large.