Linda MOHAND OUSSAÏD - 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 - FranceConception et vérification formelles des IHMsmultimodales : application à la multimodalité en sortie Modèle formel de fission sémantiqueObjectif. L'introduction des systèmes interactifs informatisés dans les systèmes critiques (industries à risques, transports, médecine) exige un grand niveau de fiabilité pour les IHM, Syntaxececi, a motivé les travaux de modélisation et de vérification formelles des systèmes I ::= UIE | (op , op )(I, I) | It(n, I) avec n ∈ Ntemp seminteractifs multimodaux. Des travaux ont été consacrés à la multimodalité en entrée au sein Où :du LISI (N. Kamel, 2006), notre travail s’intéresse à la multimodalité en sortie, sa – op ∈ TEMP = {An, Sq,Ct,Cd, Pl,Ch, In}.tempproblématique revient donc à : – op ∈ SEM = {Cc,Cp,Cr, Pr, Tr}.semSémantique statique• Proposer un modèle conceptuel formel pour la conception d’une IHM multimodale en 2sortie. ∀ i ∈ I ∃ (deb(i ), fin(i)) ∈ Time tel que deb(i ) < fin(i ) et T(i ) =(deb(i ), fin(i ))i i i i i i i iSémantique dynamique• Proposer des transformations dans des modèles permettant la vérification formelle de propriétés de sûreté et d’utilisabilité. T(i ) = (deb(i ), fin(i )) ssi op = An et fin(i ) < deb(i )k i j temp i jT(i ) = (deb(i ), fin(i )) ...

Informations

• Publié par: Omkou
• Nombre de lectures: 334
• Langue: Français

Extrait

École Nationale Supérieure de Mécanique et d’Aérotechnique /Université de Poitiers

Laboratoire 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 - France

Conception et vérification formelles des IHMs

multimodales : application à la multimodalité en sortie

Participants

• Yamine AÏT-AMEUR

• Mohamed Ahmed NACER (USTHB-Alger, [e-mail])

• Linda Mohand OUSSAÏD (CERIST-Alger, [e-mail])

Objectif.

L'introduction des systèmes interactifs informatisés dans les systèmes critiques

(industries à risques, transports, médecine) exige un grand niveau de fiabilité pour les IHM,

ceci, a motivé les travaux de modélisation et de vérification formelles des systèmes

interactifs multimodaux. Des travaux ont été consacrés à la multimodalité en entrée au sein

du LISI (N. Kamel, 2006), notre travail s’intéresse à la multimodalité en sortie, sa

problématique revient donc à :

• Proposer un modèle conceptuel formel pour la conception d’une IHM multimodale en

sortie.

• Proposer des transformations dans des modèles permettant la vérification formelle de

propriétés de sûreté et d’utilisabilité.

Pour cela, nous nous basons sur le modèle conceptuel WWHT (What, Which, How, Then)

(Rousseau, 2006) enrichi par l’introduction d’opérateurs supplémentaires, pour lequel nous

proposons un modèle formel pour les deux premières étapes (fission sémantique,

allocation) du processus de génération de la présentation multimodale en sortie.

Syntaxe

I

::=

UIE

| (

op

temp

,

op

sem

)(

I

,

I

) |

It

(

n

,

I

)

avec n

∈

N

Où :

–

op

temp

∈

TEMP

= {

An

,

Sq

,

Ct

,

Cd

,

Pl

,

Ch

,

In

}.

–

op

sem

∈

SEM

= {

Cc

,

Cp

,

Cr

,

Pr

,

Tr

}.

Sémantique statique

∀

i

i

∈

I

∃

(

deb

(

i

i

),

fin

(

i

i

))

∈

Time

2

tel que

deb

(

i

i

) <

fin

(

i

i

) et

T

(

i

i

) =(

deb

(

i

i

),

fin

(

i

i

))

Sémantique dynamique

T

(

i

k

) = (

deb

(

i

i

),

fin

(

i

j

))

ssi op

temp

=

An et fin

(

i

i

) <

deb

(

i

j

)

T

(

i

k

) = (

deb

(

i

i

),

fin

(

i

j

))

ssi op

temp

=

S q et fin

(

i

i

) =

deb

(

i

j

)

T

(

i

k

) = (

deb

(

i

i

),

fin

(

i

j

))

ssi op

temp

=

Ct et deb

(

i

i

) <

deb

(

i

j

) <

fin

(

i

i

)

T

(

i

k

) = (

deb

(

i

i

),

fin

(

i

i

))

ssi op

temp

=

Cd et deb

(

i

i

) <

deb

(

i

j

) <

fin

(

i

j

) <

fin

(

i

i

)

T

(

i

k

) = (

deb

(

i

i

),

fin

(

i

i

))

ssi op

temp

=

Pl et deb

(

i

i

) =

deb

(

i

j

)

∧

fin

(

i

i

) =

fin

(

i

j

)

i

k

=

i

i

∨

i

k

=

i

j

ssi op

temp

=

Ch

T

(

i

k

) = (

deb

(

i

k

),

fin

(

i

k

))

ssi op

temp

=

In

iter

(

n

,

i

i

) = (. . . ((

i

i

Sq i

i

)

Sq i

i

) . . .

Sq i

i

)

n fois

Modèle formel de fission sémantique

Type concurrent

I

::=

UIE

| (

op

temp

,

op

sem

)(

I

,

I

) avec

op

temp

∈

{

Ct

,

Cd

,

Pl

} et

op

sem

∈

{

Cc

}

Type alterné

I

::=

UIE

| (

op

temp

,

op

sem

)(

I

,

I

) |

It

(

n

,

I

)

avec n

∈

N,

op

temp

∈

{

An

,

Sq

,

Ch

} et

op

sem

∈

{

Cp

,

Cr

,

Pr

,

Tr

}

Type synergique

I

::=

UIE

| (

op

temp

,

op

sem

)(

I

,

I

) avec

op

temp

∈

{

Ct

,

Cd

,

Pl

} et

op

sem

∈

{

Cp

,

Cr

,

Pr

,

Tr

}

Type exclusif

I ::= UIE

| (

op

temp

,

op

sem

)(

I

,

I

) |

It

(

n

,

I

)

avec n

∈

N avec

op

temp

∈

{

An

,

Sq

,

Ch

} et

op

sem

∈

{

Cc

}

Modèle formel de fission sémantique paramétré selon l’espace CASE

Syntaxe

PM

::=

PME

| (

op

′

temp

,

op

′

sem

)(

PM

,

PM

) |

It

′(

n

,

PM

)

avec n

∈

N

Où :

–

op

′

temp

∈

TEMP

′ = {

An

′,

S q

′,

Ct

′,

Cd

′,

Pl

′,

Ch

′,

In

′}.

–

op

′

sem

∈

S EM

′ = {

Cc

′,

Cp

′,

Cr

′,

Pr

′,

Tr

′}.

PME

::=

affect

(

UIE

) |

iter

(

n

,

PME

) |

affect

(

UIE

)

compl PME

|

affect

(

UIE

)

redon PME

|

affect

(

UIE

)

choix PME avec n

∈

N

Avec :

affect

:

UIE

→

ITEM

Et ITEM

= {(

mod

i

,

med

j

)

tel que mod

i

∈

MOD

∧

med

j

∈

MED

∧

mod

i

rest med

j

}

Sémantique statique

∀

pme

i

∈

PME

∃

(

deb

′(

pme

i

),

fin

′(

pme

i

))

∈

Time

2

tel que

deb

′(

pme

i

) <

fin

′(

pme

i

)

et

T

′(

pme

i

) = ((

deb

′(

pme

i

),

fin

′(

pme

i

))

–

mode

(

med

i

)

∈

{

visuel

,

auditif

,

TPK

}.

–

partag

(

med

i

)

∈

{

true

,

false

}.

–

priorite

(

mod

i

)

∈

N.

–

priorite

(

mode

k

)

∈

N.

Sémantique dynamique

iter

(

n

,

pme

i

) = (. . . ((

pme

i

Seq pme

i

)

Seq pme

i

) . . .

Seq pme

i

)

pme

k

=

pme

i

Seq pme

j

⇒

T

′(

pme

k

) = (

deb

′(

pme

i

),

fin

′(

pme

j

))

pme

k

=

pme

i

Choix pme

j

⇒

pme

k

=

pme

i

∨

pme

k

=

pme

j

Modèle formel d’allocation

Perspectives.

Le modèle formel proposé permet de :

• Concevoir formellement une IHM multimodale en sortie par raffinement successifs (modèle

de fission, modèle d’allocation).

• Concevoir formellement l’IHM selon l’espace CASE (modèle de fission paramétré, modèle

d’allocation).

Plusieurs prolongements de ce travail peuvent être envisagés, parmi lesquels :

• Définir d’autres instanciations du modèle proposé sur d’autres espaces de conception ou

autres approches de description d’IHM multi-modales.

• Définir des propriétés génériques garantissant la qualité des IHM modélisées.

• Proposer des transformations, préservant la sémantique du système modélisé, qui

prolongent une modélisation suivant le modèle proposé dans une technique formelle cible qui

supporte la vérification des propriétés.

Vérification formelle des propriétés.

Le modèle formel proposé doit permettre de vérifier

certaines propriétés de sûreté relatives à la cohérence de la présentation multimodale et

d’utilisabilité telles que la flexibilité et la robustesse. Deux approches sont envisagées :

• Une approche basée sur la logique qui consiste à modéliser formellement l’IHM (automates

…) et à exprimer les propriétés à vérifier dans une logique particulière et de vérifier que le

modèle du système satisfait les propriétés attendues.

• Une approche par simulation qui consiste à exprimer aussi bien le système que les

propriétés dans le même langage

(automates …)

et à s’assurer que les comportements relatifs

aux propriétés désirées sont inclus dans les comportements du système.

Conception et architecture :

Utilisateur

Environnement

Système

Temps

Contexte

Noyau

fonctionnel

Contrôleur

de dialogue

Modèle de

fission sémantique

UIE

1

UIE

2

UIE

n

PM

1

PM

2

PM

n

Modèle d’allocation

PM

Modèle formel de conception et de vérification d’une IHM multimodale en sortie (Rousseau 2006)

I

Information