Timed automata based analysis of embedded system architectures

We show that timed automata can be used to model and to analyze timeliness properties of embedded system archi-tectures. Using a case study inspired by industrial practice, we present in detail how a suitable timed automata model is composed. Exact upper bounds on the timeliness properties can be found with the Uppaal model checker for a num-ber of usage scenarios. We compare our results with three other performance modeling techniques. This comparison shows that if the state space of the model is tractable, Up-paal gives the most accurate results at similar cost. The pro-posed modeling strategy can be automated, which alleviates the difficulty and error-proneness of manually constructing timed automata models.