Description du groupe MFDL

Titre du groupe

MFDL : Méthodes Formelles dans le Développement Logiciel

Responsable(s)

Aurélie Hurault, Akram Idani, Virginie Wiels

aurelie.hurault@enseeiht.fr, Akram.Idani@imag.fr, virginie.wiels@onera.fr

Aurélie Hurault
IRIT/ENSEEIHT
2 Rue Charles Camichel. BP 7122
31071 TOULOUSE CEDEX 7
email : aurelie.hurault@enseeiht.fr

Akram Idani
LIG, Domaine universitaire
681 rue de la Passerelle - BP 72
38402 Saint Martin d'Hères Cedex
email : akram.idani@imag.fr

 

Virginie Wiels
ONERA-DTIM
2 Avenue Edouard Belin. BP 4032
31055 Toulouse CEDEX
email : virginie.wiels@onera.fr

Thématique scientifique

La thématique scientifique du groupe MFDL est la modélisation et le développement formel de systèmes, qu’ils soient logiciels, matériels ou mixtes, ainsi que les vérifications et validations qui résultent de ces modélisations. Le groupe s'intéresse à la totalité du cycle de vie, depuis l’analyse des besoins jusqu’aux phases de maintenance et de déploiement.

Par approches formelles nous entendons à la fois des théories mathématiques bien fondées, mais également des méthodes, en tant que processus de construction, développement et correction des logiciels. Ces théories et méthodes conduisent naturellement

à la réalisation d'outils expérimentaux ou intégrés à des plates-formes existantes. Ce groupe a pour objectif de faire collaborer des équipes travaillant sur différents formalismes de spécification et différentes techniques de vérification et validation. Le groupe s’intéresse également à l’utilisation conjointe de méthodes formelles et de méthodes semi-formelles. Ce groupe est donc complémentaire de groupes plus ciblés (techniques de tests, validation par automates, systèmes de types, …) et permet l’échange entre différentes communautés des approches formelles.

Les problèmes scientifiques abordés par les équipes du groupe MFDL sont principalement relatifs aux orientations suivantes :

  • les approches qui permettent de construire et développer les logiciels et les systèmes de manière formelle à partir des spécifications, et par des techniques de raffinements (essentiellement la méthode B)

  • les approches formelles de validation a posteriori, par des techniques de test ou d'animation

  • des approches plus dédiées centrées sur des problématiques spécifiques ou émergeants (analyse des besoins, sécurité, ...)

    L'intérêt de regrouper les équipes et les thèmes est de favoriser les interactions entre les groupes et de faciliter la synergie et l'intégration des techniques. C'est ainsi que l'on trouve des travaux d'intégration entre les méthodes formelles et les méthodes graphiques (B et UML par exemple);

    l'utilisation des méthodes formelles pour l'explicitation des besoins et la validation des cahiers des charges; la génération des tests à partir de spécifications;

    la spécification formelle de politiques de sécurité et la vérification des logiciels par rapport à ces politiques; les spécifications formelles dans des domaines autres que les logiciels (réglementations, documents normatifs, droit, etc.) …

    Equipes participantes :


    ENST : Sylvie Vignes

    Nom de l'équipe : département INFRES; groupe : Systèmes, Logiciels,

    Laboratoire (éventuellement numéro d'UMR) UMR 5141 - labo LTCI :

    Laboratoire de Traitement et de Communication de l'Information

    Tutelles du laboratoire CNRS-GET/TélécomParis

    voir l'URL http://www.ltci.enst.fr/

    nombre de permanents: 10

    nombre de doctorants : 8


    IRIT : Mamoun Filali

    Nom de l'équipe ACADIE

    Laboratoire (éventuellement numéro d'UMR) IRIT UMR 5505

    Tutelles du laboratoire CNRS UPS INP

    nombre de permanents : 11

    nombre de doctorants et post-doctorants 6


    LORIA DEDALE : Jeanine Souquières

    Nom de l'équipe : DEDALE

    Laboratoire (éventuellement numéro d'UMR) : LORIA, UMR 7503

    Tutelles du laboratoire: Trois Universités: UHP, Nancy 2 et INPL, CNRS,

    INRIA LOrraine

    nombre de permanents : 3

    nombre de doctorants : 5

    nombre de post-doctorants :1


    LORIA MOSEL : Dominique Cansell, Dominique MERY, Stephan MERZ

    Nom de l'équipe : MOSEL

    Laboratoire (éventuellement numéro d'UMR) LORIA UMR 7503

    Tutelles du laboratoire Université Henri Poincaré Nancy 1, Université Nancy 2, INPL, CNRS, INRIA

    nombre de permanents: 6

    nombre de doctorants: 5

    post-doctorants: 1


    Heudiasyc Compiegne : Jean-Louis BOULANGER

    Nom de l'équipe : ASTRID

    Laboratoire (éventuellement numéro d'UMR) : Laboratoire HEUDIASYC (www.hds.utc.fr) UMR CNRS 6599

    Tutelles du laboratoire : Université de technologie de compiègne CNRS

    nombre de permanents, nombre de doctorants et post-doctorants : 3 permanents, 1 thésard, 3 post-docsde postdocs


    IBISC - RMF : Marc AIGUIER, Pascale LEGALL et Pascal POIZAT.

    Nom de l'equipe : Réseaux et Méthodes Formelles (RMF)

    Laboratoire : Informatique, Biologie Intégrative et Systèmes Complexes (IBISC, FRE 2873 CNRS)

    Tutelles: CNRS, Université d'Evry Val d'Essonne, Le laboratoire fait aussi partie de Genopole

    nombre de permanents : 4 PR + 1 MCF HDR + 4 MCF

    postdoc : 0, ATER docteur : 1, doctorants : 9


    LIG-Vérimag : Marie-Laure Potet

    Nom de l'équipe : LIG-VASCO, Vérimag DCS

    Laboratoire : LGI - UMR 5217, Vérimag UMR 5104

    Tutelles : CNRS, INRIA, INP Grenoble, Université Joseph Fourier, Université Pierre Mendès France

    nombre de permanents : 10 permanents, 5 doctorants, 2 postdoc


    LINA : Christian Attiogbé

    Nom de l'équipe : COLOSS (Composants et Logiciels Sûr)

    Laboratoire : LINA FRE CNRS 2729

    Tutelles du laboratoire : Université de Nantes, Ecole des Mines de Nantes, CNRS

    Nombre de permanents, nombre de doctorants et post-doctorants :

    5 permanents

    LACL : Régine Laleau

    Nom de l'équipe : Logique et Complexité

    Tutelles du laboratoire : CNRS – Université Paris 12

    Nombre de permanents, nombre de doctorants et post-doctorants : 2 permanents, 3 doctorants

    ESTAS : Georges Mariano

    Tutelles du laboratoire : INRETS – Ministère des transports

    Nombre de permanents, nombre de doctorants et post-doctorants : 18 permanents, 10 doctorants

    LAMIH : Vincent Poirriez

    Nom de l'équipe: ROI-SID

    Laboratoire (éventuellement numéro d'UMR) : Laboratoire d'Automatique, de Mécanique et

    d'Informatique, industrielles et Humaines (LAMIH - UMR CNRS 8530)

    Tutelles du laboratoire : CNRS-MIPPU et Université de Valenciennes et du Hainaut Cambrésis

    Nombre de permanents, nombre de doctorants et post-doctorants : 2 permanents, 1 doctorant


    LISI/ENSMA : Yamine AIT AMEUR

    Nom de l'équipe : Ingénierie des Données

    Laboratoire (éventuellement numéro d'UMR) : LISI/ENSMA- EA 1232

    Tutelles du laboratoire : Ministère de l'éducation Nationale et ENSMA-Poitiers.

    nombre de permanents, nombre de doctorants et post-doctorants. 3 permanents, 6 doctorants.



    SIC : Agnès ARNOULD et Laurent FUCHS

    Nom de l'équipe : Modélisation Géométrique et Animation

    Laboratoire (éventuellement numéro d'UMR) : Signal, Image, Communications (ex FRE 2731)

    Tutelles du laboratoire : Université de Poitiers

    nombre de permanents, nombre de doctorants et post-doctorants : 9 permanents et 8 doctorants

    ont 4 permanents et 2 doctorants directement intéressés par les méthodes formelles.


    LIFC : Alain Giorgetti

    Nom de l'équipe : TFC (Techniques Formelles et à Contraintes)

    Laboratoire (éventuellement numéro d'UMR) : LIFC, FRE 2661

    Tutelles du laboratoire: Université de Franche-Comté, CNRS, INRIA

    Nombre de permanents : 14

    Nombre de doctorants : 10

    Nombre de post-doctorants : 1


    CEDRIC : Catherine Dubois

    Nom de l'équipe : CPR

    Laboratoire (éventuellement numéro d'UMR) : CEDRIC, EA 1395

    Tutelles du laboratoire : Ministere

    nombre de permanents , nombre de doctorants et post-doctorants : 9 permanents, 2 thésards,


    LIP6 : Mikal Ziane

    Nom de l'équipe : MoVe

    Laboratoire : LIP6

    Tutelle :

    nombre de permanents , nombre de doctorants et post-doctorants : 4 permanents, 3 doctorants


    GET/ENST Bretagne : Nora et Frédéric CUPPENS

    Nom de l'équipe : SERES (Sécurité des Réseaux et des Systèmes d'Informations)

    Laboratoire (éventuellement numéro d'UMR) : GET/ENST Bretagne, département RSM

    Tutelles du laboratoire : GET, ministère de l'industrie

    nombre de permanents: 4

    nombre de doctorants: 8

    post-doctorants: 1


    CEA-LIST : Bruno Marre

    nombre de permanents: 5

    nombre de doctorants: 1


    ONERA-DTIM : Virginie Wiels

    Nom de l'équipe DTIM

    lABORATOIRE (éventuellement numéro d'UMR) : ONERA (DGA, Ministère de la Défense)

    nombre de permanents : 20

    nombre de doctorants et post-doctorants : 6 doctorants, 1 post-doctorant


    PRISM : Nicole Lévy

    Nom de l'équipe : SFAL (Spécifiation formelle et architecture logicielle )

    Laboratoire (éventuellement numéro d'UMR) : PRiSM, UMR CNRS 8144

    Tutelles du laboratoire : Université de Versailles St-Quentin en Yvelines et CNRS

    nombre de permanents : (de l'équipe) 2

    nombre de doctorants et post-doctorants (de l'équipe et intéressés par le groupe): 1


    IRISA : Jean-Marc Jezequel

    Nom de l'équipe : Triskell

    Laboratoire (éventuellement numéro d'UMR) : Irisa (UMR 6074)

    Tutelles du laboratoire : INRIA, CNRS, U. Rennes 1, INSA Rennes

    nombre de permanents impliqués : 3

    nombre de doctorants et post-doctorants (de l'équipe et intéressés par le groupe): 3

     

    Equipes étrangères ou industrielles associées au groupe de travail

    Pierre-Yves Schobbens - FUNDP - Namur
    Marc Frappier - Université de Sherbrooke

    Bill Stoddart, Steve Dunne, Teesside, UK

    Richard Bannach, Manchester, UK

     

    Les industriels associés à MFDL sont les partenaires habituels avec lesquels les équipes du groupe ont l’habitude de travailler. En particulier les utilisateurs et développeurs industriels de la méthode B participent régulièrement aux journées du groupe.

    Objectifs du groupe de travail - Projets d’actions

    L'objectif est de continuer à souder et à développer cette communauté tout en élargissant les thématiques concernées. La liste des participants montre à la fois l'intérêt des anciens partenaires de continuer cette collaboration mais aussi certaines

    ouvertures (nouvelles équipes et apparition de nouveaux domaines comme la modélisation de politiques de sécurité).Ceci se fera à travers des journées thématiques. A l’occasion des études de cas ou des expérimentations communes pourront

    être proposées, comme ceci a été fait pour l’étude de cas. Contrôle d’accès (http://www-lsr.imag.fr/afadl2000/EtudeDeCas).

     

    Mode de fonctionnement - Organisation des activités du groupe

    En dehors des rencontres liées à la conférence AFADL, le but est de proposer des journées thématiques. On prévoit deux catégories de journées:

    • des journées transversales, destinées à faire mieux connaître les personnes et les travaux des différentes équipes. Ce peut être des journées de présentation de travaux de doctorants, ou des journées bilan de projets ANR/ACI, par exemple.

    • des journées thématiques ciblées sur des techniques ou sur une problématique, qui pourront faire l'objet d'une publicité auprès de nos partenaires industriels et où nous pourrons inviter des spécialistes du sujet.

      Conférences ou ateliers associés au groupe

      Le groupe est à l'origine de l'Atelier francophone AFADL :

      Les résultats de cet atelier ont fait l’objet de plusieurs efforts de diffusion. Les actes de chaque édition sont distribués aux participants et archivés sur les sites web successifs de la conférence. Chaque atelier a donné lieu à un numéro spécial de TSI.

      Page Web

      http://afadl.cnrs.fr

      liste de diffusion : afadl-alp@imag.fr