Model-Based Design for Embedded Systems- P17: 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. | 136 Model-Based Design for Embedded Systems order to handle preemptive scheduling strategies. This made the timed-automata model of a task less natural than one could wish. 4. A fourth model used stopwatch automata rather than clocks to model the timing of tasks which allows preemption to be dealt with in a more natural way. In general the reachability problem for stopwatch automata is undecidable and the Uppaal support for stopwatches is based on overapproximations. But our experiences with using this model were good In the examples we have tried so far the results were always exact the verification was more efficient compared with the previous model typically 40 faster and it used less space and we can thus verify larger systems than with the previous model. We are currently working toward a model that will reduce the number of clocks used compared to the four models mentioned above. The goal is to have just one clock for each processing element and achieving this we expect a major efficiency gain for the verification. Using the MoVES Analysis Framework In order to make the model usable for system designers details of the timed-automata model are encapsulated in the MoVES analysis framework. The system designer needs to have an understanding of the embedded system model but not necessarily of the timed-automata model. It is assumed that tasks and their properties are already defined and therefore MoVES is only concerned with helping the system designer configure the execution platform and perform the mapping of tasks on it. The timed-automata model is created from a textual description that resembles the embedded system model presented in Section . MoVES uses Uppaal as back-end to analyze the user s model and to verify properties of the embedded system through model checking as illustrated in Figure . Uppaal can produce a diagnostic trace and MoVES transforms this trace into a task schedule shown as a Gantt chart. As MoVES is a framework aimed at .
