COMPOSITE TIMED-SERVICE AUTOMATA

55

There are two different approaches to design timed-service automata:

1. Treating service as external function and time as an internal function.

2. Treating time as external function and service as an internal function.

Design Approach:

1. Treating service as external function and time as internal function:

In the automata design, here time is written explicitly as a transition function for each state change but service is not explicitly defined. A separate automaton is defined for each service offered by this machine.

2. Treating time as external function and service as internal function:

In the automata design, here service and time are written explicitly as a transition function for each state change. A single automaton may be defined or one automaton for each service offered may be defined.

2. ∀ ∈time threshold value of (F^TS1)∩TC^TS2pre , a ∈ κ(TC^TS2_pre) is the precondition of TS2 denoted by predicates.

= 1 ⊗ 2 = < , ∑ , , , , , >is the composition defined by:

3. TC^TS= <TC^TS1pre, TC^TS1eff∪TC^TS2eff>

4. ∑^TS=∑^TS1∪∑^TS2 5. Q^TS= Q^TS1 Q^TS2

= < , > | ∈ 1 ∧ 2 ∧ ∀ ∈ ( 1 / 2 )}

6. = × ∑ ⟶

={( , ) ⟶ ( ′, ′)| ⟶ ′∧ ∈ ∑ 1 ∧ 1 ∩ 2 ≠

∅∀ ∈ 2/ 1} ∪ {( , ) ⟶ ( ′, ′)| ⟶ ′∧ ∈

∑ 2 ∧ 1 ∩ 2 ≠ ∅ ∧ ∀ ∈ 1/ 2}

7. = {( , )| ∈ 1 ∧ ∈ 2 ∧ ∀ ( 1/ 2)} ∈ 8. = {( , )| ∈ 1 ∧ ∈ 2 ∧ ∀ ∈ ( 1/ 2)} ∈

9. = ⟶ Range of threshold values

= 1 ∪ 2

To form a composition of two automata we always need to have a prerequisite that both the automata are independent or the second one is dependent on the first one but cannot happen the other way round i.e the first one is dependent on the second automata. When a composite automaton is formed the time threshold has to be carefully used such that it is applicable

57

to both the services individually as well as combined state. Hence, it is better to provide a range of threshold values which suit the condition and then choose one value within the range since it is always difficult to specify a single value for time.

Whenever we form a composition of two automata we take the cross product of the states of both the automata to define the new states of the automata (this is to ensure that all the combinations are covered). Also, the initial state is a pair (x,y) where x is the initial state of automata 1 and y are the initial state of automata 2. Similarly, the final state is a pair (x,y) where x is the final state of automata 1 and y are the final state of automata 2. There can always be a single initial state for the automata but there can be one or more final states. The set of all final states of automata is a subset of the states of the automata. The initial state and the final state cannot be NULL. When we define a state (x,y) for the composite automata we have a threshold value t1 associated with x and threshold value t2 associated with y, we define the new threshold value by putting a / as follows t1/t2. A precondition and an effective/post condition are defined for each state of the automata.

The new precondition of the composite automata is not dependent on the second automata. The effective condition is a union of the effective conditions of both the automata. Only if the effective condition is satisfied the automata move into the next state else it will be looping in the same state. With respect to the above Timed automata definition, UPPAAL could be used to validate and verify the working. Three windows are available namely the editor, simulator and the verifier. To start with the automata is constructed in the editor. Here UPPAAL template could be used to create the

automata initially by using drag and drop options. Also, transitions between the various states can be depicted. Different global declarations, process assignment and system definition can be also be done in the editor.

Figure 3.5 UPPAAL tool verifying the automata for concurrency

Figure 3.5 illustrates a screen shot from the UPPAAL verification tool.

“Guard” parameter could be used to specify the threshold value satisfaction condition for the transitions. A local clock function is used to track all the states. In the simulator window, transitions can be enabled to see the working. Also, variable view and system view can be differentiated. In the verifier window, we can select the states for which we need to test (The

59

entire automata or a subset can be tested). If the automata constructed are optimal then it will change to the next state else it will keep looping in the same state. Also, the requirements can be specified and can be matched whether the given model meets the requirements or not. If satisfied, then it is displayed in green. Figure 3.5 is a screen shot of the tool which is used to verify the automata for its concurrency.

A timed automaton is a finite automaton with an additional clock variable attached. These values of clock variables are always real and synchronous.

UPPAAL views several timed automata in parallel assuming mutual independence. Each automaton consists of several states and there is a state change whenever an action is performed or there is a change in the clock variable. UPPAAL provides several additional features which could be attached to the timed automata. One important feature which is required for our scenario is the “guard” which evaluates to a Boolean value. This is mainly used to keep track of whether the threshold value is reached or not.Both modeling and verification of the automata can be done using UPPAAL. We have a separate window called verifier where we can prove the correctness of the automata modeled.The simulator window mainly consists of four parts:

1. Control part: Transitions can be enabled here and they can also be chosen. Also toggling between simulation is allowed here.

2. Variable view: Here we can view the various constraints and also the values of clock variables.

3. System view: Gives the complete picture of all automata and also the current active states.

4. Message sequence chart: Depicts the synchronization between different processes.

Table 3.4 A comparison of Automata(A), Service Automata(SA) and Timed Automata(TA)

Context Attributes Finite set of actions Set of States Set of Transitions Initial states Final States Assignment Function Clocks

Automata - ∑ Q Δ q0 F - -

Service

Automata C ∑ Q Δ I F V -

Timed

Automata - ∑ Q T I F X

Timed- Service Automata

C ∑ Q T I F V X

SA -Transition function (δ) TA - Transition function (T)

ak g,a,Y

(δ) = qiqj qiqj

a_{k =}set of actions g = clock constraints

a = set of actions Y = subset of clocks qi= state: immediate predecessor

qj= state: immediate successor of the action ‘a’

The comparison of the three automata theory as presented in Table 3.4 supports this research by raising the need for timed-service automata.

Though in literature there is evidence of using both service and timed

61

automata in context-aware service composition, it does not cater to the requirements of the research problem that has been discussed here. The following chapter elaborates the context-aware framework that has been proposed and also explains the implementation of the algorithm in detail.

Chapter 4

Context-aware