The test oracles consist of properties that must be checked. Properties may be related to funtional and multimodal interactions requirements. In this section the CARE properties can be expressed as lustre expression and the can be included in an automatic test oracle.

Equivalence

Two modalities Ml and M2 are equivalent w.r.t. a set T of tasks, if every task t Î T can be activated by an expression along Ml or M2. Let EAMl be an expression along modality Ml and let EAM2 be an expression along M2. EAMl or EAM2 can activate the task ti Î T. Therefore, equivalence can be expressed as follows.

OnceFromTo (EAMl or EAM2, not ti, ti)

Where OnceFromTo(A, B, C) specifies that property A must hold at least once between the instants where events B and C occur.

Redundancy and Complementarity

In order to define the two properties Redundancy and Complementarity that describe combined usages of modalities, we need to consider the use over time of a set of modalities. For both Redundancy and Complementary, the use of the modalities may occur simultaneously or in sequence within a temporal window Tw, that is, a time interval. To specify the temporal window in Lustre, they consider C to be the duration of an execution cycle (time between reading an input and writing an output). The temporal window is then specified as the number of discrete execution cycles