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 général, "explicite" signifie clairement exprimé (visiblement) alors que "implicite" signifie indirectement exprimé ou impliqué. Notons que dans le génie logiciel, la signification de ces termes fait apparaître des inconsistances. En analyse des besoins, ces termes sont utilisés pour distinguer l'expression déclarative (descriptive) et opérationnelle (prescriptive) des besoins. Cette phase d'analyse consiste à générer des besoins explicites (de niveau type) et déclaratifs à partir de besoins implicites (de niveau instance ou scénario). Le besoin de méthodes formelles pour une telle génération est avéré. En conséquence, les travaux visés par IMPEX consistent à traiter formellement les termes implicites et explicites dans le processus d'ingé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.

Abstract of the project

All software systems execute within an environment or context. Reasoning about the correct behavior of such systems is a ternary relation linking the requirements, system and context models. Formal methods are concerned with providing tool (automated) support for the synthesis and analysis of such models. These methods have quite successfully focused on binary relationships, for example: validation of a formal model against an informal one, verification of one formal model against another formal model, generation of code from a design, and generation of tests from requirements. The contexts of the systems in these cases are treated as second-class citizens: in general, the modeling is implicit and usually distributed between the requirements model and the system model. This project proposal is concerned with the explicit modeling of contexts as first-class citizens.

In general usage, "explicit" means clearly expressed or readily observable whilst "implicit" means implied or expressed indirectly. However, it should be noted that there is some inconsistency, within the computer science and software engineering communities, regarding the precise meaning of these adjectives. The requirements engineering community use the terms to distinguish between declarative (descriptive) and operational (prescriptive) requirements where they acknowledge the need for a formal method for generating explicit, declarative, type-level requirements from operational, instance-level scenarios in which such requirements are implicit. A consequence of our research will be a formal treatment of the adjectives implicit and explicit when engineering software.

Nowadays, several research projects and approaches aim at formalizing mathematical theories that are applicable in the formal developments of systems. These theories are helpful for building complex formalizations, expressing and reusing proof of properties. Usually, these theories are defined within contexts, that are imported and and/or instantiated. They usually represent the implicit semantics of the systems and are expressed by types, logics, algebras, etc. based approaches.

To our knowledge, no work adequately addresses the formal description of domains expressing the semantics of the universe in which the developed systems run. For example, the context dependent properties (like weight which depends on gravity) are not expressed in the formal theory in which the formal developments are conducted. This domain information is usually defined in an explicit semantics.

Several relevant properties are checked by the formal methods. These properties are defined on the implicit semantics associated to the formal technique being used: type checking, proofs theory, logic based reasoning, rewriting, refinement, model checking, trace analysis, simulation, etc. When considering these properties in their context with the associated explicit semantics, these properties may be no longer respected. As a very simple example, take two formally developed systems that are composed to exchange currency data represented by a float. This system is no longer consistent if one system refers to Euros and the other to dollars. This is due to the absence of explicit semantics' expression in the proof context of the system defining this composition. Therefore, the development activities need to be revisited in order to be able to handle not only the implicit semantics, but also these that are explicit. Without a more formal software engineering development approach, based on separation of implicit and explicit, the composition of software components in common contexts risks compromising correct operation of the resulting system. This is a significant problem if we wish to develop dynamic systems of heterogeneous components that are reliable (self-healing) in unreliable contexts. Thus, this project is about separation of intrinsic and extrinsic concerns by building explicit formal models of contextual semantics using proof based techniques and illustrated on diverse application domains.