MORSE: Méthodes et Outils pour la Vérification Formelle de Systèmes Intéropérables Embarqués critiques

Nouvelles fraîches

• 16/07/2006:
  • Nouveaux documents dans l'espace privé
• 12/06/2006:
  • Nouveaux documents dans l'espace privé
  • Artgicle REE sur MORSE en ligne
• 10/05/2006:
  • Nouveaux documents dans l'espace privé
• 23/12/2005:
  • Nouveaux documents dans l'espace privé
  • Nouveaux documents dans l'espace "fournitures" (livrables pour Décembre 2005)
• 10/12/2005:
  • Nouveaux documents publics et publications
• 09/09/2005:
  • Nouveaux documents dans l'espace privé
• 11/07/2005:
  • Nouveaux documents dans l'espace privé
• 08/07/2005:
  • Nouveaux documents dans l'espace privé
• 30/06/2005:
  • Nouveaux documents dans l'espace privé
• 10/01/2005:
  • Nouveaux documents dans l'espace privé
• 31/12/2004:
  • Nouveaux documents dans l'espace public (posters et publications)
  • Nouveaux documents dans l'espace "fournitures" (livrables pour Décembre 2004)
• 16/07/2004:
  • Nouveaux documents dans l'espace privé
• 10/07/2004:
  • Nouveaux documents dans l'espace privé
  • Articles publiés dans l'espace public.
• 13/04/2004:
  • Nouveaux documents (document Aonix + article soumis et accepté à la conférence RSP'2004)
• 01/04/2004:
  • Nouvelle version du compte-rendu de la réunion du 06/032/2004 enrichie de celui de la réunioin technique partielle du 17/02/2004 (espace privé)
  • Compte-rendu de la réunion du 09/03/2004 (espace privé)
• 09/02/2004:
  • Compte-rendu de la réunion du 06/02/2004 (espace privé)
• 26/01/2004:
  • Mise en place de la livraison associé au semestre 1 dans l'espace "fournitures" (accès protégé)
• 26/12/2003:
  • Mises à jour mineures (documents dans l'espace privé), premier document dans l'espace livraisons (à valider)
  • Ajout du modèle latex pour les documents MORSE (sous la forme d'un "package" prêt à l'emploi)
• 21/12/2003:
  • restructuration de l'espace privé suivant les modalités de la réunion du 19/12/2003
  • ajout d'un espace "fournitures" vide
  • ajout d'une version anglaise pour la partie publique

Introduction

L’objectif du projet MORSE est de fournir une solution pour le développement d’applications industrielles certifiables dans le secteur de l’avionique et plus particulièrement pour les drones Cette classe d’applications est caractérisée par les contraintes suivantes :

• des exigences fortes de fiabilité,
• la nécessité de certifier l’application,
• la capacité à s’exécuter dans un environnement réparti ne disposant que de communications asynchrones.

Compte tenu du contexte industriel du projet, MORSE doit fournir une méthodologie outillée guidant le développement des applications définies ci-dessus et permettant d’atteindre le niveau de qualité exigé dans l’avionique.

La méthodologie proposée et outillée par MORSE repose sur les cinq points suivants :

• une approche par prototypage centrée sur la notion de modèle,
• l’utilisation systématique des méthodes formelles,
• la synthèse automatique de programmes depuis les spécifications formelles,
• un langage pivot assurant la cohérence entre les étapes de la conception,
• la réutilisation de spécifications existantes.

L’approche par prototypage est courante dans l’industrie. La méthodologie construite dans le cadre de MORSE sera utilisée dans ce contexte, elle doit donc être intégrable dans un processus de développement maîtrisé. Le prototypage s’appuie sur la notion de modèle (exprimé dans un formalisme rigoureux) qui constitue un “fil conducteur” de la spécification d’une solution à sa réalisation. Néanmoins, dans le cadre d’applications réparties, cette méthode trouve ses limites. Il est en effet très difficile voire impossible de prendre en compte au niveau du prototype l’ensemble des comportements possibles du logiciel, la sémantique d’un tel modèle n’étant pas complètement opérationnelle.

Les méthodes formelles apportent une réponse à ce problème, ce qui justifie leur utilisation dans le cadre de MORSE. Leurs fondements mathématiques permettent d’exprimer les propriétés attendues du logiciel et de les prouver. Dans le cadre d’un processus de certification, les preuves de propriétés sont un moyen performant pour aider à la mise en conformité avec la norme. Le modèle formel sera le point de départ de l'analyse formelle et de la construction des prototypes. Une combinaison de plusieurs techniques est envisagée : représentation compacte de l’ensemble des états accessibles en utilisant les Diagrammes de Décision de Données , vérification modulaire et réduction du modèle en fonction des propriétés étudiées. D’autre part, les méthodes structurelles offertes par un formalisme comme les réseaux de Petri permettent de vérifier certaines propriétés sans que le calcul de l’espace des états soit nécessaire. Ces deux approches (model checking et analyse structurelle) seront utilisées de manière complémentaire dans MORSE.

La synthèse automatique de programmes consiste en la génération automatique du squelette distribué de l’application. Le code produit permettra la construction rapide de prototypes pour l’évaluation immédiate de la solution proposée. À la fin du cycle de développement du logiciel, le code généré sera déployable en exploitation sur la plate-forme visée. MORSE se focalise donc sur la génération du code gérant la répartition et l'asynchronisme, propriétés reconnues comme difficiles à implémenter.

Afin d’assurer le lien entre les phases de la méthodologie proposée, MORSE introduit un langage pivot. Ce langage permettra d’exploiter les informations d’une spécification UML. Il aura également une sémantique formelle pour supporter l’analyse de modèles et les capacités d’un langage de description d'architecture pour relier les composants de l'application. Les travaux autour de LfP (Language for prototyping) développé au LIP6 fournissent une première base pour ce langage pivot.

Un prototype d’Atelier de Génie Logiciel (AGL) sera réalisé dans le cadre du projet MORSE, ce prototype implémentera la méthodologie proposée. Il sera utilisé pour le développement d’une application témoin déployée sur la plate-forme de drones de SAGEM.

SAGEM s’est entouré de plusieurs partenaires (AONIX, le LIP6 et le LABRI) choisis en fonction de leurs compétences et de leur complémentarité dans les domaines couverts par MORSE.

• AONIX est une société de conseil et un éditeur reconnu d’environnement de développement dans le domaine des applications critiques. Cette société est présente, entre autres, dans les secteurs avionique, ferroviaire et automobile.
• Les partenaires universitaires (le LIP6 - Laboratoire d'Informatique de Paris VI - et le LaBRI – Laboratoire Bordelais de Recherche en Informatique) ont mené de nombreuses recherches sur les méthodes formelles et leurs applications, de plus ces deux équipes sont spécialisées dans l’étude des systèmes répartis et asynchrones.

L’ensemble des partenaires forme un groupe cohérent dont les membres ont déjà collaboré au cours de travaux antérieurs.

Contacts