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.%検証済みのモデルから実時間プログラムを生成する手法を提案する．本手法では，時間制約を実行時に検査するために，それに伴うオーバーヘッドをあらかじめモデルの性質の一部に取り入れる．これにより，実時間スケジューラのないOSやランタイム上でのソフト実時間システムの実現を容易にすることを目指す．本稿では，時間オートマトンで記述され，モデル検査券UPPAALで検証されたモデルから，JavaおよびCのコードを生成する手法について述べる．簡単なロボットの制御プログラムの記述例を通して，提案手法の有効性を示す．