| 研究課題/領域番号 |
08780260
|
|---|
| 研究種目 |
奨励研究(A)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
結縁 祥二 名古屋大学, 工学部, 助手 (70230612)
|
|---|
| 研究期間 (年度) |
1996
|
| 研究課題ステータス |
完了 (1996年度)
|
| 配分額 *注記 |
1,100千円 (直接経費: 1,100千円)
1996年度: 1,100千円 (直接経費: 1,100千円)
|
|---|
| キーワード | 実時間システム / 通信プロセスモデル / 並行システム / 検証技法 / CCS / SCCS / 抽象モデル / 形式意味論 |
|---|
| 研究概要 |
本年度は,以下の項目について研究を行った。
●実時間通信プロセスのテスト擬順序に対する証明技法の開発
実時間通信プロセスモデルを既存の通信プロセスモデルを拡張して定義し、従来直接扱うことのできなかった量的な時間の概念を計算モデルに導入した。この拡張モデルにおいて、テスト擬順序による意味論を展開し、その証明技法を正則なクラスに対して確立した。ここでは、時間は実数領域を用いるため、無限の状態が存在するが、正則な実時間通信プロセスでは、振舞いが変化するポイントは、その記述から記号的に有限に表現できることに着目して、証明技法を提案した。
●命令レベル並列プロセッサ向きのコンパイラ仕様記述
実時間性をもつ通信プロセスでモデルの応用として、RISCプロセッサのような演算ユニットを複数有する計算プロセッサに対するコンパイラの振舞いを、同期的な並行計算の記述体系であるSCCS[Milner'83]を用いて抽象的に記述した。ここでは、命令レベル並列プロセッサを資源、その上で実行されるプログラムを消費者とみなし、並行システムとして定式化した。コンパイラの記述では、タイミングが本質的であるので動作の実時間性が要求される。この定式化によって、細部に立ち入らずにコンパイラの振舞いを記述でき、論理的なレベルでコンパイラの検証を行うことができるようになった。さらに、効率的な仕様検証のために、SCCSが表現するラベル付き遷移システムの効率的構成法についても検討したい。
|
