Information Technology Reference
In-Depth Information
state Q , then the state composed of P |||Q transits by a to state P |||Q :
P −−→ P
P |||Q a
Q −−→ Q
P |||Q a
−−→ P |||Q
−−→ P |||Q
is an operator borrowed from Lotos. Conversely to the
previous operator, which only enables a single action to be executed at a time, parallel
operator
- Parallel operator
||
authorizes the execution of an action of the first system or even an action of
the system or these two actions at the same time. We have imposed a condition on the
modalities of actions put in parallel. We will consider that a modality cannot produce
two actions at the same time.
||
P a
Q a
−−→ P
P ||Q a
−−→ Q
P ||Q a
−−→ P ||Q
−−→ P ||Q
−−→ P and Q a 2
a 1
−−→ Q and modality( a 1 ) = modality( a 2 )
P ||Q a 1 ,a 2
P
−−−−→ P ||Q
4.4.3. Verified properties
Once the HCI is modeled and the system of transitions describing its dynamic
behavior is generated, the verification of these properties can be carried out according
to two techniques. The CARE properties are part of the properties of usability of
the multimodal HCI, thus two formal models were defined for CARE. The first is
operational and it describes the property with a system of transitions [KAM 07]. This
model is based on the same syntaxical and semantic elements as those used for the
model of multimodal interactions presented in the previous section. The technique of
verification used in this case is based on the comparison of transition systems of the
multimodal HCI and the property that needs to be verified.
The second model is logical and describes the properties by the declarative
expression in a logic interpreted in a transition system. In this model, the verification
is carried out with the help of the model checking technique. Two techniques were
tested: the SMV ( symbolic model verifier ) technique [MCM 92], where the properties
are expressed in the CTL temporal logic [KAM 04, KAM 05]; and the Promela/Spin
technique [HOL 91], where the properties are expressed in the LTL temporal logic
[PNU 77]. In this section, we present the expression of CARE properties in LTL
logic with the SPIN tool. For this we will go ahead with the abstraction of actions of
interaction by replacing each of the actions by the modality that generates it. Thus,
the variable mod is introduced. It contains the value of the modality that enabled the
interactive action that labeled the transition to be carried out.
 
Search WWH ::




Custom Search