時相論理と並行計算、オートマトンの統合化による自律性のある分散システムの設計支援

2001 年度 実績報告書

• 研究課題/領域番号: 11680360
• 研究機関: 金沢大学
• 研究代表者: 山根 智 金沢大学, 工学部, 助教授 (70263506)
• キーワード: 分散システム / 開放型システム / 実時間処理 / ハイブリッドモデル / receptiveness / 詳細化検証 / 仕様記述 / 計算機支援

研究概要

平成13年度では、前年度の成果の上に、以下のような成果を得た:
1.無限状態モデルにおける実時間型開放分散システムにおいて、以下の提案及び開発を行った。
(1)前年度開発した詳細化検証の公理系を改善した。具体的には、抽象度の高い仕様と低い仕様との間の詳細化関係を定義する詳細化写像の意味付けを形式化した。これにより、以下が明らかになった:
・1991年にAbadiらが開発したリアクティブシステムの詳細化検証理論と等価であることが明らかになった。
・提案した詳細化検証は時間模倣関係の検証であることが明らかになった。
(2)改善した詳細化検証の公理系を計算機上に実現した。これはプロトタイプであるが、簡単な事例を対象として、本手法の有効性を確認した。
2.ハイブリッド型開放分散システムにおいて、以下の提案及び開発を行った。
(1)ハイブリッド型モデルによる仕様記述書語を開発した。これは、環境との相互作用が表現できるハイブリッド型計算モデルであり、より強力にアナログ動作が表現できる。
(2)上記の仕様記述言語で記述したシステムのreceptivenessの検証手法を開発した。
(3)さらに、上記の仕様記述言語で記述したシステムの詳細化検証手法を開発した。
以上の(1)-(3)により、ハイブリッド型開放分散システムの設計支援の基礎を開発できた。
今後の課題としては、以上の開発した手法を本格的に計算機に実装して、大規模問題への適用及びその評価がある。

研究成果

• [文献書誌] 山根 智: "ハードリアルタイムシステムの形式的仕様記述と形式的検証"情報処理学会論文誌. Vol.42, No.6. 1623-1635 (2001)
• [文献書誌] 山ノ口 崇, 山根 智: "Deductive Refinement Verification Methods based on Assume-Guarantee Style and their Experimental Evaluations of Real-Time Software"2nd International Conf. on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computeing. 2. 254-261 (2001)
• [文献書誌] 山根 智: "ハイブリッドシステムのモジュール演繹的検証手法"電子情報通信学会研究報告. CST2001-4. 21-28 (2001)
• [文献書誌] 山根 智: "ハイブリッドシステムの高信頼性設計方法論"電子情報通信学会研究報告. FTS2001-71. 17-24 (2001)
• [文献書誌] 山根 智: "ハイブリッドシステムの詳細化理論による組込み型システムの開発方法論"電子情報通信学会研究報告. SS2001-40. 7-14 (2002)
• [文献書誌] 山根 智: "Modular Specification and Verification Method for Hybrid Real-time Systems"Proc. International Conference on Real-Time Computing Systems and Applications, IEEE Computer Society. 8. 201-208 (2002)