Intégration des sémantiques implicite et explicite dans les développements de systèmes discrets fondés sur la preuve. – IMPEX

Les systèmes logiciels évoluent et s'exécutent dans un environnement ou contexte. Raisonner sur la correction de leur comportement repose sur une relation ternaire entre les modèles de besoins, de systèmes et de contexte. Les méthodes formelles offrent des outils (automatiques) pour la synthèse et l'analyse de tels modèles et se sont intéressées à des relations binaires : validation d'un modèle vis-à-vis d'un modèle informel, vérification d'un modèle formel vis-à-vis d'un modèle formel, génération de code à partir d'un modèle, génération de tests à partir de besoins, etc. Le contexte, dans ces cas, est traité comme de seconde classe : en général il est implicite et réparti entre besoins et modèles. IMPEX vise à rendre explicite la modélisation des contextes et des environnements associés à des domaines d'application.
En ge´ne´ral, "explicite" signifie clairement exprime´ (visiblement) alors que "implicite" signifie indirectement exprime´ ou implique´. Notons que dans le ge´nie logiciel, la signification de ces termes fait apparaître des inconsistances. En analyse des besoins, ces termes sont utilise´s pour distinguer l'expression de´clarative (descriptive) et ope´rationnelle (prescriptive) des besoins. Cette phase d'analyse consiste a` ge´ne´rer des besoins explicites (de niveau type) et de´claratifs a` partir de besoins implicites (de niveau instance ou sce´nario). Le besoin de me´thodes formelles pour une telle ge´ne´ration est ave´re´. En conse´quence, les travaux vise´s par IMPEX consistent a` traiter formellement les termes implicites et explicites dans le processus d'inge´nierie du logiciel ou des systèmes.
Plusieurs approches et projets de recherche traitent de la formalisation de théories mathématiques utilisées pour le développement formel de systèmes. Ces théories contribuent à la construction de formalisations complexes exprimant et réutilisant des preuves de propriétés. En général, ces théories sont définies au sein de contextes qui sont importés ou instanciés. Elles offrent un cadre pour représenter la sémantique implicite du système à développer et sont fondées sur la logique, algèbres, théorie des types, etc.
A notre connaissance, il n'existe pas de travaux qui traitent, de manière intégrée, de la description formelle de domaines constituant des contextes dans lesquels les systèmes évoluent. Par exemple, les propriétés dépendant du contexte (poids dépendant de la gravité) ne sont pas exprimées dans la théorie où les développements sont menés. Ce type d'information est exprimé dans une sémantique explicite.
Plusieurs propriétés importantes sont vérifiées en méthode formelle. Elles sont définies et vérifiées à partir de la sémantique implicite associée à la technique formelle utilisée : contrôle de types, preuve, réécriture, raffinement, model checking, analyse de traces, simulation etc. Lorsque ces propriétés sont traitées dans leur contexte en leur associant une sémantique explicite, elles peuvent ne plus être valides. Un exemple est la composition de systèmes échangeant des flottants représentant des monnaies exprimées en dollars dans l'un et en euros dans l'autre. L'absence de sémantique explicite dans le contexte de preuve rend cette composition invalide. Ainsi, les activités de développement doivent être reconsidérées en fonction de la possibilité de représenter non seulement la sémantique implicite mais aussi la sémantique explicite. La formalisation de ces opérations de développement en séparant l'implicite de l'explicite renforcerait la correction des systèmes ainsi développés. Cet aspect constitue un problème significatif si l'on souhaite développer des systèmes dynamiques, à base de composants hétérogènes fiables, dans des contextes qui ne le sont pas.
Ainsi, IMPEX traite de la séparation des aspects intrinsèques et extrinsèques en permettant la construction des modèles formels de contextes par l'utilisation des méthodes formelles fondées sur la preuve au travers de deux domaines d'application.