Preuve de programmes. Processus IDM
Validation des algorithmes en UML et OCL

Placée en phase terminale d'un processus de développement IDM où les modèles représentent une certaine abstraction des exigences des applications à développer, la programmation est souvent considérée comme une simple activité de génération de codes issus des modèles.

Comment, dans ces conditions, peut-on prouver que tout programme fonctionne correctement et que les exigences des applications ont été bien prises en compte ?

Cette étude traite de propriétés formelles des langages de programmation dont le but est de raisonner sur des programmes pour chercher à vérifier et prouver qu'ils fonctionnent correctement. Le rajout de propriétés axiomatiques au niveau des langages de modélisation permet ainsi de vérifier que les modèles ont toutes les qualités que l'on peut en attendre de leur part. Les propriétés axiomatiques, appliquées dans le contexte d'un processus IDM vu comme une succession de transformations de modèles permettent donc de vérifier la cohérence de l'ensemble des modèles et des programmes.

Cette étude se situe dans la continuité de la sémantique opérationnelle des langages de programmation décrivant de manière précise et rigoureuse les aspects comportementaux de leurs constructions syntaxiques spécifiées à l'aide d'une grammaire. Elle prend donc toute son importance pour des applications ayant des exigences très critiques, telles qu'on en trouve aujourd'hui dans des domaines d'activités très variés, de l'aéronautique et de l'espace par exemple, ou pour des applications « grand public » de l'administration et de la banque devant gérer des masses de données personnelles et privées. La confiance que l'on doit accorder à ces logiciels est d'autant plus importante qu'ils doivent fonctionner comme des automates pour être réactifs en temps réel aux différents environnements qu'ils sont chargés de contrôler, de gérer et de superviser et pour être disponibles 24 h sur 24 aux sollicitations des usagers au travers de téléprocédures.

Après avoir rappelé comment on peut raisonner sur des programmes à l'aide de propriétés basées sur la logique (propriétés axiomatiques) pour vérifier et prouver qu'ils ont un fonctionnement correct, nous montrons ensuite comment on peut définir et appliquer de telles propriétés pour vérifier que les modèles situés en amont d'un processus de développement ont bien les qualités attendues. Comment, dès lors, appliquer de telles propriétés lors de la spécification des traitements d'un système ou d'un sous-système décrits à l'aide de langages de modélisation métier, tel que SAM dédié au développement d'applications de l'aéronautique ?

Peut-on contribuer à obtenir une meilleure continuité entre les modèles et les programmes d'un processus de développement en proposant d'appliquer les mêmes approches de raisonnement et de preuve basées sur la logique des prédicats ? C'est la question qui est en fait posée dans cet article.