Microcontroller Assembly Synthesis from Timed Automaton Task Specifications

A method for the automatic refinement of single-task timed automaton specifications into microcontroller assembly code is proposed. The outputs of the refinement are an assembly implementation and a timed automaton describing its exact behaviour. Implementation is only possible when all specified timing behaviours can be met by the target microcontroller. Crucially, the implementation does not make the simplifying synchrony assumption, yet correctness with respect to timing is guaranteed. Currently this method copes with parallel inputs and outputs, but is restricted to timed automaton specifications with only one clock variable that is reset after each transition. Further generalization is possible. A tool illustrates the method on a simple example.