Information Technology Reference
In-Depth Information
automatically builds a generator of test data for the program being tested. In these
works, the CARE properties were specified in Lustre; then verified with the help of
the Lutess tool. These works do not use formal methods during the design of the
system but they call on it at the end of the multimodal system development in order to
carry out software tests.
Method B [ABR 96], in its event-driven version, was used in the [AIT 06b,
AIT 06a] works for formalizing the specifications of an operational interactive
system all the while ensuring certain ergonomic properties. The system was modeled
by a set of guarded events (the event is then set off as soon as its guard is fulfilled).
The properties were expressed in the form of invariants (properties always needing
to be checked) in the higher order logic. The authors have proposed a development
methodology based on refinement [AIT 06b] and a validation of tasks expressed with
the CTT process algebra [AIT 06a]. A representation of the CARE properties in B
was also addressed in [AIT 06a].
4.4.2.
A general formal model for input multimodality
In this section, we present a formal model of the design of the input multimodal
interaction put forward in [KAM 06]. It is meant to be used in the design phase in the
development life cycle of a multimodal interactive system. It is a model that formalizes
the refined CASE space informally defined in [BEL 92, BEL 95]. A formal model
inspired by the algebra of the CCS process [MIL 80] and Lotos is defined for each
multimodal HCI class of this space. The syntax of the model is given by grammar rules
and semantics of the words of this grammar are given by labeled transition systems.
4.4.2.1.
Syntax
The syntax of the model is given by grammar containing two rules. The first rule
S
is used to generate the model according to the user tasks from a high level of
abstraction to an elementary level, which are the statements. The latter are tasks that
set off an elementary function of the functional core of the application. The second rule
E
generates the statements by composing basic interactive actions (which cannot be
broken down):
a
of set
A
representing the interactive actions of the system.
Am
i
is the
set of actions produced by modality
m
i
. The basic interactive actions, the statements
as well as the tasks are composed with the help of a set of operators: ;,
, [],
||
and
that respectively refer to prefixing, sequence, choice, the parallel operator and
interleaving. The symbol
δ
is used to designate the stopping or end of a process. The
semantics of these operators is presented later.
|||
4.4.2.2.
Types of HCI
Exclusive type
: in this type of interface, the statements are produced in a sequential
manner. This implies that the parallelism operator must not be used to compose the
