Passer au contenu

Technologie : les méthodes formelles ont un impact sur le cycle de développement logiciel

La suppression des tests unitaires et de validation est conditionnée à l’emploi de la preuve tout au long du cycle.

Contrairement aux tests, qui n’interviennent qu’après la phase de codage, les méthodes formelles avec preuves accompagnent l’ensemble du cycle de développement logiciel. Y compris lors du passage du cahier des charges ?” ou modélisation physique ?” à la spécification technique, souvent considéré par les experts comme le maillon faible de la chaîne. Car la transcription de l’un vers l’autre dans un langage différent augmente le risque d’erreurs. De fait, il est généralement nécessaire de reformuler le cahier des charges, en vue de sa formalisation, au sein d’une spécification générale. Celle-ci est ensuite décomposée en propriétés successives pour constituer au final une spécification technique structurée. Durant le déroulement de cette étape, dite de raffinement, il est prouvé que chaque propriété ?” ou modèle ?” nouvellement construite n’introduit aucune incohérence avec celle de niveau supérieur. Le résultat est la formalisation de toutes les propriétés du système. L’étape suivante consiste alors à transformer les modèles abstraits obtenus en modèles concrets. Ceux-ci contiennent des variables pouvant être traduites dans un langage informatique classique. La preuve, qui intervient tout au long de ce processus, est l’élément essentiel qui remet en cause les tests. Elle garantit non seulement la cohérence des éléments constitutifs du système, mais aussi que, lors de l’introduction de chacun d’entre eux, aucun ne remet en cause le travail déjà effectué. Les adeptes des méthodes formelles estiment que la preuve offre une plus grande garantie d’exhaustivité que celle procurée par les tests, qualifiés d’approximatifs. Dans un cycle en V, la preuve a un impact sur les parties basses du cycle. Elle autorise donc la suppression des tests associés aux phases de spécification et de conception ?” soit, respectivement, les tests de validation et les tests unitaires. Mais les tests globaux demeurent toujours d’actualité. Ils permettent de valider, pour leur part, la partie haute du cycle en V. En loccurrence, le cahier des charges.

🔴 Pour ne manquer aucune actualité de 01net, suivez-nous sur Google Actualités et WhatsApp.


Jean-Marie Portal