On Generating Realtime Programs with Runtime Checking From Timed Automata to Realtime Programs on Non-Realtime Environments

摘要

We propose a method of generating realtime programs from verified models. The primary goal of this work is to provide an easy way of constructing soft realtime programs running in environments that do not provide realtime features. To realize this, the timing constraints described in a model should include properties of the runtime overhead and the generated code checks its timing constraints at runtime. In this paper, we describe how to generate plain Java/C programs from timed automata that are model-checked using UPPAAL.