本論文は実時間ステートチャートのためのプロセス言語による，同期 動作記述から実時間並行システムの設計支援を行う形式的な枠組を示 す．実時間ステートチャートは並行性，階層性を持つことでシステム 全体の振舞いを記述できるため，頻繁に用いられる．しかし，実時間 ステートチャートは形式的に動作意味が定義されていないため，形式 的動作意味を定義する．
実時間ステートチャートに対する形式的意味論としてLüttgenらの 提案したステートチャートのためのプロセス言語SPLを時間遷移を用 いて拡張したSPLRTを定義する．SPLはラベル付き遷移システム によりステートチャートの振舞いを記述し，SOS(構造動作意味定義 )によりその遷移を定義する．SOSの規則により動作遷移，クロック遷 移を定義する．動作遷移はイベントにより遷移が発生し，実時間ステー トチャートの内部計算を扱う．クロック遷移は同期遷移ラベルがつけ られた遷移であり，動作遷移により発生した遷移を外部的に一度に発 生させる．SPLRTではSOSの規則に遅延遷移を新たに定義 し，稠密時間遷移を表現した．遅延遷移を加えることでイベントの発 生時刻を区別することができ，実時間ステートチャートにおける時間 制約の解釈を明示的に判断できる．
実時間ステートチャートにより記述された実時間システムの例を SPLRTにより動作定義し，シミュレーションにより時間軸に沿っ た実時間ステートチャートの振舞いを示すことができた．実時間ステー トチャートの振舞いをSPLRTを用いて記述することにより SPLRTの実時間ステートチャートに対する正当性を示した．