Mickael BARON - These

Baronm

Description

École Nationale Supérieure de Mécanique et d’Aérotechnique /Université de PoitiersLaboratoire d’Informatique Scientifique et Industrielle (www.lisi.ensma.fr)ENSMA - Téléport 2-1 Avenue Clément Ader - BP 40109 - 86961 FUTUROSCOPE CHASSENEUIL Cedex - FranceVers une approche sûre du développement des Interfaces Homme-MachineEnjeuxEnjeuxDéveloppement, validation et Les interfaces homme-machine (IHM) constituent une vérification de systèmes interactifspart indispensable dans la quasi-totalité des systèmes Approches fondées sur le Approches fondées sur informatiques. Le recours à des modèles de développement formel la définition d’outilsspécification, de développement, de vérification et de validation devient indispensable. Aujourd’hui les Model Based SystemsConstructeurs UIApproches existantes Systèmes de preuvesapproches fondées sur le développement formel et les • Spécification de • Outils d’aide à la approches fondér la définition d ’outils peuvent • CNUCE (Lotos) • Model Checkingmodèlesêtre mises en parallèle pour la vérification de propriétés. conceptionCNUCE, CERT, ICO• York (Z)• Génération UIMalgré des avancées intéressantes, aucune d’elles • Absence de prise en • Theorem Proving• ICO (Réseaux de Petri)n’est encore parvenue à s’imposer. compte de l’utilisateur • MASTERMIND, York et LISI• LISI (Méthode B) MOBI-D, Petshop• JBuilder, Visual .NETL’objectif général de nos travaux consiste à améliorer • CERT (Lustre)l’utilisation de méthodes formelles dans ...

Informations

• Publié par: Sioc
• Nombre de lectures: 65
• Langue: Français

Extrait

École Nationale Supérieure de Mécanique et d’Aérotechnique / Université de Poitiers Laboratoire d’Informatique Scientifique et Industrielle(ww.wil.fr)si.ensma ENSMA - Téléport 2-1 Avenue Clément Ader - BP 40109 - 86961 FUTUROSCOPE CHASSENEUIL Cedex - France

Vers une approche sûre du dé veloppement des Interfaces Homme-Machine

Enjeux Développement, validation et p L a e r s t    i i n nt d e i r s f p a e c n e s s  ab h l o e  m d m a e n - s  m l a a  c q hi u n a e s   i- ( t I o H ta M li ) t   é co d n e s s t   it s u y e s n t t è   m un e e s     vérification de systèmes interactifs informatiques. Le recours à des modèles de Approches fondées sur le Approches fondées sur spécification, de développement, de vérification et de développement formel la définition doutils validation devient indispensable. Aujourd’hui les approches fondées sur le développement formel et les  Model Based Systems  Systèmes de preuves  Constructeurs UI Approches existantes approches fondées sur la définition d ’outils peuvent  de Spécification  Outils     daide à la    CNUCE (Lotos)  Checking Model être mises en parallèle pour la vérification de propriétés.  conception  modèles  CNUCE, CERT, ICO  York (Z) n M ’e al s g t  r e é nc d o e r s e    p a a v r a v n e c n é u e e  s à   s i ’ n i t m ér p e o s s s e a r. ntes, aucune d’elles  IMDNTSRE, ratiGénéI MA onU CO(Ia  uxRéseteiredP) TorherPmenivog predceenbsA d siene c  sateurlutili L’objectif général de nos travaux consiste à améliorer eodthMé IBD-O B M ) ILSI IS(IL iVlauliuB,redE r T o . Y N tek motpee Pe,hot  s J p l’utilisation de méthodes formelles dans le cadre du  CERT (Lustre)  s développement et de la validation des applications interactives. - Nous cherchons à réaliser un pont entre les modèles Limites des approches existantes et les notations de modélisation des tâches de ces mêmes méthodes. LISI (Méthode B)  Model Based Systems - Nous étudions la définition d’outils reposant sur des  Absence de validation de tâches utilisateurs  propriétaires  Modèles méthodes formelles, et destinés à des non spécialistes  doutils daide à la validation Peu de ces mêmes méthodes.

Résultats Coopération entre approche formelle et approche outils V fo al r id m at e i ll o e n Conction(Modèledarchitecture) Validation ep expérimentale Résultats Résultats Technique de Système Vérification & Tâches utilisateur opé P r r a o te p u o r s s i  ti d' o u n n d e e a  l m gè o b d r é e li  s d a e t  i p o r n o  c d e e s s s  us Tutsheâcuetasili TTC r VéVriafliicdaattiioonn& rcpidse f  ro itno llme Génération sel séba rsudèmo Validation CTT gratIntédunion an  d leel apeuns inhcetemrofeuq ilutsocprohe e (concurrence, choix, interruption, Raffinement Environnement complet ve désactivation, ...)  ntB E nctiostraAb SUIDT (simulateur, animateur, ...) Extension es Modélisation de systèm de taille  Pas de phase de génération explicite Preuvesdepr a o r p b r i i t é r t a é i s r  e surlestâches tiliesuur CT sate T hcâT oitacifiréV nioatidal & V n ircsed e noitp ecTdueiqhn Génération é Système bas Vérificatioonn& Tâches utilisateur Validati CTT formelle sur modèles utilisateur

Approche formelle Approche outils Raffinement Abstraction Deuxi T è â m c e h  e n e i 1 ve  a > u > d  e T m âc o h d e é 2 lisation  SUIDT (Safe User Interface Development Tool) Outil Codage de lopérateur activation Bemllmeneloppéfor nel déve noitcnofuayonudurtemaniA Premier niveau de  t en modélisation Tâche0 REFINivationRef REFINESActivation VARIABLESy j MODELActivation INVARIANTJ(x i , y j ) &EtatAct : (0..2) &I’(y j ) VARIABLESx i INITIALISATIONInit(y j ) |EtatAct := 2 INVARIANTI(x i ) ASSERTIO G 0 N (x S i )    > (G 0 ’(y j ) & EtatAct = 0) or (G 1 (y j ) & EtatAct = 2) or = INIT … nItix( i ) EVENTS (G 2 (y j ) & EtatAct = 1) EVENTS Evt 0 =SEEvt 1 =SELECT Evt 2 =SELECT LECT   Evt 0 =SE G L 0 E ( C x i T ) G & 0 y tE ’( j c ) t= atA G 0 & 1 (y E j  G t)atAct = 2 & 2 tE (y j ta ) 1 =tcA THEN THEN  THEN THEN S 0 (x i ) S 0 ’(y j ) | S 1 (y j ) S | 2 (y tE j ) :t =tacA END; END0 END END  EN END Outils de simulation pour tion et ér ication Introduction de nouveaux événements Environnement SUIDT disponible en téléchargement  if v lala valida qui modélisent les tâches 1 et 2 à ladressetth:p//ww.wilise.snma.fr/ihm

Perspectives

Les recherches menées actuellement s’intéressent à la fois à lemenhissnricetet à l’étude de latiratévicpéoo ’ des deux approche. Concernant le premier point (l’enrichissement), nous étudions principalement la faisabilité des approches sur différents domaines d’application. Ainsi, nous pensons que l’utilisation de l’approche fondée sur le B événementiel est adaptée au domaine de la multi-modalité. Cet aspect est actuellement traité dans le cadre d’un projet RNRT VERBATIM.  Enfin, concernant le second point (la coopérativité) nous pensons définir unetémedohpour chacune des approches et la manière de combiner à la fois l’approche formelle et l’approche outils dans un processus de développement.

Participants • Yamine AÏT-AMEUR • Mickaël BARON • Patrick GIRARD