通信プロセスモデルにもとづく実時間並行プログラムの検証と実現に関する研究

Research Project

Project/Area Number	08780260
Research Category	Grant-in-Aid for Encouragement of Young Scientists (A)
Allocation Type	Single-year Grants
Research Field	計算機科学
Research Institution	Nagoya University
Principal Investigator	結縁祥二名古屋大学, 工学部, 助手 (70230612)
Project Period (FY)	1996
Project Status	Completed (Fiscal Year 1996)
Budget Amount *help	¥1,100,000 (Direct Cost: ¥1,100,000) Fiscal Year 1996: ¥1,100,000 (Direct Cost: ¥1,100,000)
Keywords	実時間システム / 通信プロセスモデル / 並行システム / 検証技法 / CCS / SCCS / 抽象モデル / 形式意味論
Research Abstract	本年度は,以下の項目について研究を行った。 ●実時間通信プロセスのテスト擬順序に対する証明技法の開発実時間通信プロセスモデルを既存の通信プロセスモデルを拡張して定義し、従来直接扱うことのできなかった量的な時間の概念を計算モデルに導入した。この拡張モデルにおいて、テスト擬順序による意味論を展開し、その証明技法を正則なクラスに対して確立した。ここでは、時間は実数領域を用いるため、無限の状態が存在するが、正則な実時間通信プロセスでは、振舞いが変化するポイントは、その記述から記号的に有限に表現できることに着目して、証明技法を提案した。 ●命令レベル並列プロセッサ向きのコンパイラ仕様記述実時間性をもつ通信プロセスでモデルの応用として、RISCプロセッサのような演算ユニットを複数有する計算プロセッサに対するコンパイラの振舞いを、同期的な並行計算の記述体系であるSCCS[Milner'83]を用いて抽象的に記述した。ここでは、命令レベル並列プロセッサを資源、その上で実行されるプログラムを消費者とみなし、並行システムとして定式化した。コンパイラの記述では、タイミングが本質的であるので動作の実時間性が要求される。この定式化によって、細部に立ち入らずにコンパイラの振舞いを記述でき、論理的なレベルでコンパイラの検証を行うことができるようになった。さらに、効率的な仕様検証のために、SCCSが表現するラベル付き遷移システムの効率的構成法についても検討したい。