210 VERIFICATION USING TIMED AUTOMATA

The corresponding region automaton R(A) for a timed transition table A =, S, S0, C, E is a transition table over the alphabet .

To prove that the language accepted by an automaton is nonempty, we need to show that an infinite accepting path exists in the automaton’s transition table. For a timed automaton, the timing constraints disallow certain paths in the transition table. [Alur and Dill, 1994] show that given a timed automaton, a Buchi automaton can be constructed such that the set of untimed words accepted by the Buchi automaton is the same as the one obtained by the Untime operation on the timed words accepted by the timed automaton. They provide an algorithm for checking emptiness for timed automata with clock constraints containing only integer constants.

Untimed automata are extended with clock variables and timing constraints on transitions to yield timed Buchi automata (TBAs), which can represent time regular processes. Then to allow the analysis of TBAs with infinite extended states, corresponding region automata are introduced.

The verification algorithm can verify the correctness of finite-state real-time systems. TBAs model finite-state real-time systems. The objective is to check that the implementation of a real-time system meets the specification of this system. Both the implementation and the specification are first represented by timed automata. Then we prove the desired inclusion, that the language accepted by the implementation automaton is a subset of the language accepted by the specification automaton.

Given a timed process (A, L) where L is a language over the alphabet P(A), if L is a timed regular language, then this is a timed regular process representable by a timed automaton. Usually, an implementation is represented by a TBA AI that is a composition of n components with each component described by a timed regular process Pi = (Ai , L(Ai )). The system specification is represented by a timed regular language S over the alphabet P(A), where A = A1 · · · An . The system is said to be correct iff the following inclusion is satisfied: L(AI ) S.

EXERCISES

1.Use an MMT automaton to specify the simple railroad crossing with one train rail, described and specified using RTL in chapter 6.

2.Using the notations in the Lynch–Vaandrager approach, show a timed trace of a timed execution of the automaton in exercise 1.

3.Explain the differences between the Lynch–Vaandrager timed automaton and the MMT automaton.

4.Use a single clock to respecify the example climate control system in Figure 7.1.

5.Show a run of the timed transition table for the automaton in exercise 2.

6. Suppose there are two clocks (i and j) in a timed transition table, ci = 2 and

c j = 3. Show all clock regions.

7.How does a region automaton make it possible to represent an infinite number of time-extended states in a finite representation?

EXERCISES 211

8.Construct the region automaton for automaton α3 in Figure 7.4.

9.Specify the hospital intensive care unit monitoring subsystem in chapter 6 (exercise 2) as an Alur–Dill timed automaton.

10.Specify the smart airbag deployment system described in chapter 4 (exercise 6) as an Alur–Dill timed automaton. Compare the expressiveness and space requirement for the timed automaton model and the timed transition graph model.