La conception des applications logicielles est une tâche délicate qui requiert la prise en compte d'un ensemble d’aspects (concurrence, communication, comportement hybride,…) et l’intégration d’un ensemble d’activités particulières.
[...]
Le travail présenté dans ce manuscrit, tire partie de l'Ingénierie Dirigée par les Modèles (IDM), d'UML, des méthodes formelles, des systèmes multi-agents et des frameworks afin de proposer un processus de conception intégrant des aspects de spécification, de vérification et d'implantation. Il se fonde sur la réalisation de trois modèles adaptés à chacune de ces activités : le modèle de spécification, le modèle de vérification et le modèle d'implantation (Figure 1). Dans ce contexte, l’Ingénierie Dirigée par les Modèles offre les concepts (métamodélisation et transformations de modèles) nécessaires à l’intégration et à la manipulation de ces trois modèles au sein de l'approche proposée. En outre, les transformations de modèles permettent de réaliser la projection d'un modèle source vers différents domaines afin de profiter de leurs avantages respectifs; à partir du modèle de spécification, il est alors possible d'obtenir les modèles de vérification et d'implantation. Le modèle de spécification permet de représenter une abstraction des systèmes logiciels réactifs concurrents ; il est décrit à l’aide d’un Langage Spécifique de Domaine (ou DSL) inspiré des ADL et des diagrammes de composants d’UML 2.0. Il repose sur l'utilisation d'agents concurrents, qui communiquent à l'aide d'actions partagées et d'objets partagés ; leur comportement est conforme à une sémantique d’exécution hybride (événementiel asynchrone et continu synchrone). Le modèle de vérification permet au concepteur d’utiliser des méthodes et des techniques de vérification qui garantissent que le modèle obtenu durant la phase de spécification est conforme au comportement souhaité. En effet, dans le cas de systèmes critiques, les aspects de vivacité et de sûreté de fonctionnement sont primordiaux. Pour garantir ces aspects, nous proposons de recourir à des spécifications formelles et à des techniques formelles de vérification en modélisant le modèle de vérification à l’aide d’une algèbre de processus nommée Finite State Processes (ou FSP) pouvant être exploitée par l'outil de model-checking LTSA. Le modèle d’implantation est exprimé à l'aide de classes et de configurations d’objets; il repose sur l’utilisation d’un framework Java qui fournit un ensemble de concepts et une sémantique d’exécution proches de ceux utilisés dans le modèle de spécification. Ce faisant il permet de réduire l’écart sémantique entre la réalisation et la conception précédemment vérifiée.
