Information Technology Reference
In-Depth Information
Information
Dialog
controller
Functional core
User
Semantic
fission
Environment
UIE
1
UIE
2
UIE
n
Allocation
System
PME
1
PME
2
PME
n
Time
Instanciation
Context
Evolution
PME
1
' PME
2
'
PME
n
'
Figure 4.1.
Transitions system of the exclusive multimodal HCI
4.4.4.2.
Verification of the properties of usability
The properties of complementarity and equivalence of the two modalities
speech
and
direct handling
, for the realization of the task
fillinFrom
, have been verified in
transitions, with the help of the SPIN checker. Each property is expressed by a LTL
temporal logic formula. The two formulae are obtained by replacing in the generic
formula, the values
stateI
and
stateF
of the variable state by the values 2 and 5
corresponding to the initial and the final state of the task, as well as the modalities
values
m
1
and
m
2
of the variable mod by the values corresponding to the modalities
speech
and
direct handling
. The result of this verification concludes that the property
of complementarity is not satisfied by the exclusive type multimodal HCI, whereas the
equivalence property is fulfilled.
4.5. Use of formal methods for output multimodality
4.5.1.
Existing models
As with the multimodality in input, works have focused on modeling the design
process for multimodality in output, nonetheless the design models put forward remain
informal. We cite among these works the design space, the
Standard Reference Model
(SRM) symbol and the
What
,
Which
,
How
,
Then
(WWHT) model.
