Linda MOHAND OUSSAÏD - These
1
page
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
1
page
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
É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 )) ...
Voir
É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, anacer@cerist.dz)
• Linda Mohand OUSSAÏD (CERIST-Alger, lmohand@cerist.dz)
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
