zbMATH — the first resource for mathematics

Code synthesis for timed automata. (English) Zbl 1088.68625
Summary: We present a framework for the development of real-time embedded systems based on timed automata extended with a notion of real-time tasks. It has been shown previously that reachability and schedulability for such automata can be checked effectively using model checking techniques. In this paper, we propose to use the extended automata as design models. We describe how to compile design models to executable programs with predictable behaviours. The compiling procedure ensures that the execution of the generated code satisfies mixed timing, resource and logical constraints imposed on the design model. To demonstrate the applicability of the framework, a prototype C-code generator based on the legOS operating system has been implemented in the TIMES tool and applied to develop the control software for a production cell. The production cell has been built in LEGO$$^{\circledR}$$ equipped with a Hitachi H8 based LEGO$$^{\circledR}$$ Mindstorms control brick.

MSC:
 68Q45 Formal languages and automata
HyTech