A Formal Framework for Design and Validation of Multimodal Interactive Systems in Transport Domain - Human-Computer Interactions in Transport - page 106

- ClicNrequest : click the mouse on the button attributed to the creation of a new
request. The click on this button engenders the creation of a new window in a form for
request input.

An expression of an multimodal HCI of an exclusive type can be broken down
according to tasks as follows:

( CreateReq ) ( FillinFrom ) ( FillinTo )

Here, CreateReq is the task that enables us to create a new window to formulate a
request. FillinFrom is the task that enables the From field to be filled in, corresponding
to the town of departure in the form of the request. FillinTo is the task that enables us
to fill in the To field corresponding to the destination town. Each of these tasks can be
carried out in two different ways, which corresponds to the definition of two different
statements for the realization of each of the tasks. Each of these statements is defined
according to basic interactive actions as follows:

Create1Req = 'show me flights'; δ

Create2Req = clicNrequest; δ

Fillin1From = ClicFrom; ClicBoston; δ

Fillin2From = 'From'; 'Boston'; δ

FillinTo = ClicTo; ClicOslo; δ

Fillin2To = 'To'; 'Oslo'; δ

Finally, the expression of the multimodal HCI according to the basic actions is
obtained by replacing each of the statements by its expression according to the basic
actions:

(('show me flights'; δ )[](ClicNrequest; δ ))

(('From'; 'Boston'; δ )[](ClicFrom; ClicBoston; δ ))

(('To'; 'Oslo'; δ )[](ClicTo; ClicOslo; δ ))

The corresponding transitions system is given in Figure 4.1.

Figure 4.2 shows a part of the Promela code that implements this transitions
system.

The random variable was introduced to carry out non-determinism. The
instruction if..fi , randomly chooses the two instructions guarded by the same guard
random =1. The transitions are carried out in an uninterrupted manner with the
instruction atomic

{}

.