Model based development of real-time embedded systems has actively been studied. Generating real-time code from a model is an important topic of these studies. In this paper, we briefly describe a code generation scheme for real-time programs for non-real-time environment. The generated code runs in a runtime environment without inherent real-time scheduling facilities. In our approach, models are formally written as systems of timed automata and are verified using UPPAAL model checker prior to be processed by our code generator. In order to make the generated code to meet the timing requirements in a non-real-time environment, the code generator weaves explicit timing checking code fragments in the code. We construct a simple two-wheeled robot as a case study of this approach.
各種検索
サポート
ヘルプ