tailieunhanh - Model-Based Design for Embedded Systems- P43

Model-Based Design for Embedded Systems- P43: This book contains information obtained from authentic and highly regarded sources. Reasonable efforts have been made to publish reliable data and information, but the author and publisher cannot assume responsibility for the validity of all materials or the consequences of their use. | 386 Model-Based Design for Embedded Systems continuous systems. Timed and hybrid automata are attempts to bridge the two worlds. Although timed automata are a special class of hybrid automata their study as a separate model is justified by the fact that many problems that are very difficult or impossible to solve . undecidable for hybrid automata are easier or solvable for timed automata. Timed Automata Timed automata 9 extend finite automata by adding variables that are able to measure real time these variables are called clocks. Standard finite-state automata are able to specify that a certain set of events occur in a specific order however they do not typically specify how much time has elapsed between two successive events. Figure shows an example of a finite automaton that specifies the order between four events a b c d event a precedes b which precedes c which precedes d. This automaton has five states numbered 0-4 and four transitions labeled by the four events. State 0 is the initial state. Figure shows an example of a timed automaton TA . It is very similar to the untimed version but its transitions are annotated with additional information referring to clocks x and y. This TA specifies in addition to the order a b c d between events two timing constraints 1 the time that may elapse between a and d is at most 5 time units 2 the time that may elapse between b and c is at least 2 time units. In other words we can view the semantics of this automaton as a set of all possible sequences of occurrences of events in time timed sequences that satisfy timing constraints 1 and 2 in addition to the correct order a b c d. This is illustrated in Figure . We can also look at the semantics of this automaton in an operational way. This is illustrated in Figure . The automaton starts at state 0 and spends a certain amount of time to there. During this time the value of each clock of the automaton increases by the amount of time that has .