修士論文：
「実時間システムの構成的開発のためのπ計算に対する時間拡張」

概要

本論文では、実時間ソフトウェア開発のためのπ計算[1,2,3]に対する時間拡張を 提案し、リアルタイムオブジェクト指向言語に対し時間拡張したπ計算による記述 への変換規則を与える。

時間拡張したπ計算は時間経過とタイムアウトを表現できる。従来のπ計算に対し 決められた長さだけ時間待ちするアクションを導入する。時間の経過は構造動作 意味によって定義される特別な遷移として表す。時間の経過も含めて振舞いが同等で あれば、時間を無視しても同じように振舞うことを示す。

時間拡張したπ計算を用いて実時間ソフトウェアの振舞いを厳密に記述する。形式的 記述による動作検証を機械的に行うことができ、実装前に正しく仕様に従って振舞うか 確認することが可能になる。ソフトウェアプログラムを変換規則を使って変換する ことで時間拡張したπ計算による記述が得られる。振舞いの記述とプログラムから 変換して得られた記述を比較することで実装の正しさを確認できる。ペースメーカー の例を用いてどのような記述が得られるか示す。