2001 Fiscal Year Annual Research Report

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

Research Project

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

Research Products
(6 results)

All Other

All Publications (6 results)

[Publications] 山根智: "ハードリアルタイムシステムの形式的仕様記述と形式的検証"情報処理学会論文誌. Vol.42, No.6. 1623-1635 (2001)
[Publications] 山ノ口崇, 山根智: "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)
[Publications] 山根智: "ハイブリッドシステムのモジュール演繹的検証手法"電子情報通信学会研究報告. CST2001-4. 21-28 (2001)
[Publications] 山根智: "ハイブリッドシステムの高信頼性設計方法論"電子情報通信学会研究報告. FTS2001-71. 17-24 (2001)
[Publications] 山根智: "ハイブリッドシステムの詳細化理論による組込み型システムの開発方法論"電子情報通信学会研究報告. SS2001-40. 7-14 (2002)
[Publications] 山根智: "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)

2001 Fiscal Year Annual Research Report

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

Principal Investigator

山根 智 金沢大学, 工学部, 助教授 (70263506)

Research Products

[Publications] 山根 智: "ハードリアルタイムシステムの形式的仕様記述と形式的検証"情報処理学会論文誌. Vol.42, No.6. 1623-1635 (2001)

[Publications] 山根 智: "ハイブリッドシステムのモジュール演繹的検証手法"電子情報通信学会研究報告. CST2001-4. 21-28 (2001)

[Publications] 山根 智: "ハイブリッドシステムの高信頼性設計方法論"電子情報通信学会研究報告. FTS2001-71. 17-24 (2001)

[Publications] 山根 智: "ハイブリッドシステムの詳細化理論による組込み型システムの開発方法論"電子情報通信学会研究報告. SS2001-40. 7-14 (2002)

[Publications] 山根 智: "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)

山根智金沢大学, 工学部, 助教授 (70263506)

[Publications] 山根智: "ハードリアルタイムシステムの形式的仕様記述と形式的検証"情報処理学会論文誌. Vol.42, No.6. 1623-1635 (2001)

[Publications] 山根智: "ハイブリッドシステムのモジュール演繹的検証手法"電子情報通信学会研究報告. CST2001-4. 21-28 (2001)

[Publications] 山根智: "ハイブリッドシステムの高信頼性設計方法論"電子情報通信学会研究報告. FTS2001-71. 17-24 (2001)

[Publications] 山根智: "ハイブリッドシステムの詳細化理論による組込み型システムの開発方法論"電子情報通信学会研究報告. SS2001-40. 7-14 (2002)

[Publications] 山根智: "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)