tailieunhanh - Model-Based Design for Embedded Systems- P5

Model-Based Design for Embedded Systems- P5:The unparalleled flexibility of computation has been a key driver and feature bonanza in the development of a wide range of products across a broad and diverse spectrum of applications such as in the automotive aerospace, health care, consumer electronics, etc. | 96 Model-Based Design for Embedded Systems extended with integer variables and richer user-defined data types. A timed automaton is a finite-state machine extended with clock variables. The tool uses a dense time-model of time so clock variables evaluate to real numbers. All the clocks progress synchronously. We use in this section the train-gate example distributed with the tool . It is a railway system that controls access to a bridge. The bridge has only one track and a gate controller ensures that at most one approaching train is granted access to this track. Stopping and restarting a train takes time. Figure shows the model of a train in the editor of Uppaal. When a train is approaching Appr it must be stopped before 10 time units otherwise it is too late and the train must cross the bridge Cross . When it is stopped Stop it must be restarted Start before crossing the bridge. The timing constraints associated with the locations are invariants. They give a bound on how long these locations can be active A train can stay in Appr at most 20 time units and then must leave this location. Edges between locations have guards x 10 to constrain when they can be taken synchronizations stop id for communication and updates x 0 to reset the clock x. Automata communicate with each other by means of channels. Here we have an array of channels and every train has its own id. The gate automaton selects a train and synchronizes with it with stop id . In Uppaal it is possible to declare arrays of clocks or any other type. Channels can be declared to be urgent to prevent delays if a synchronization is possible or broadcast to achieve broadcast synchronization instead of handshake. Listing shows the global declaration of the model with the channel FIGURE View of the train template in the editor. Model-Based Framework for Schedulability Analysis Using Uppaal 97 Listing Global declarations for the train-gate model. 1 const int N 6 Number of trains 2 typedef int