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

1996 Fiscal Year Annual Research Report

• Project/Area Number: 08780260
• Research Institution: Nagoya University
• Principal Investigator: 結縁 祥二 名古屋大学, 工学部, 助手 (70230612)
• Keywords: 実時間システム / 通信プロセスモデル / 並行システム / 検証技法 / CCS / SCCS / 抽象モデル / 形式意味論

Research Abstract

本年度は,以下の項目について研究を行った。
●実時間通信プロセスのテスト擬順序に対する証明技法の開発
実時間通信プロセスモデルを既存の通信プロセスモデルを拡張して定義し、従来直接扱うことのできなかった量的な時間の概念を計算モデルに導入した。この拡張モデルにおいて、テスト擬順序による意味論を展開し、その証明技法を正則なクラスに対して確立した。ここでは、時間は実数領域を用いるため、無限の状態が存在するが、正則な実時間通信プロセスでは、振舞いが変化するポイントは、その記述から記号的に有限に表現できることに着目して、証明技法を提案した。
●命令レベル並列プロセッサ向きのコンパイラ仕様記述
実時間性をもつ通信プロセスでモデルの応用として、RISCプロセッサのような演算ユニットを複数有する計算プロセッサに対するコンパイラの振舞いを、同期的な並行計算の記述体系であるSCCS[Milner'83]を用いて抽象的に記述した。ここでは、命令レベル並列プロセッサを資源、その上で実行されるプログラムを消費者とみなし、並行システムとして定式化した。コンパイラの記述では、タイミングが本質的であるので動作の実時間性が要求される。この定式化によって、細部に立ち入らずにコンパイラの振舞いを記述でき、論理的なレベルでコンパイラの検証を行うことができるようになった。さらに、効率的な仕様検証のために、SCCSが表現するラベル付き遷移システムの効率的構成法についても検討したい。

Research Products

• [Publications] 結縁祥二: "正則な実時間通信プロセスに対するテスト擬順序の記号特性化" 電子情報通信学会論文誌. (掲載決定).
• [Publications] 鈴木晃: "命令の並列に実行するCPUに対するSCCSによるコンパイラの仕様記述" 電子情報通信学会技術報告. COMP96-14. 49-58 (1996)
• [Publications] 鈴木晃: "SCCS動作式に対するumfold変換によるLTSモデルの効率的構成法" 電子情報通信学会技術報告. COMP96-47. 93-100 (1997)