Modeling a Language for Embedded Systems in Timed Automata

Abstract

We present a compositional method for translating real-time
programs into networks of timed automata. Programs are written in an
assembly like real-time language and translated into models supported
by the tool Uppaal. We have implemented the translation and give an
example of its application on a simple control program for a car. Some
properties of the behavior of the control program are verified using the
generated model.