• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2000 年度 実績報告書

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

研究課題

研究課題/領域番号 11680360
研究機関鹿児島大学

研究代表者

山根 智  鹿児島大学, 工学部, 助教授 (70263506)

キーワード分散システム / 時相論理 / 演繹的検証 / リアルタイム性 / 詳細化検証 / Assume-Guarantee / receptive
研究概要

平成12年度では、前年度の成果の上に、以下のような成果を得た:
1.有限状態モデルにおいて、以下の提案及び開発を行った。
(1)分散システムを仕様記述可能とした拡張時間オートマトンを開発して、拡張時間オートマトンのAssume-Gurantee形式による自動詳細化検証手法を提案した。ここでの詳細化関係は、Milnerが提案した模倣関係を実時間制約で拡張した時間模倣関係である。
(2)拡張時間オートマトンで仕様記述した分散プロセスが物理的に実装可能であることを保証する条件、いわゆるreceptivenessの自動検証手法を実現した。Receptivenessは、環境と分散プロセスとの無限ゲームで形式化できる。
(3)自動詳細化検証器の実装を行って、計算機実験により、提案手法の有効性を示した。
2.無限状態モデルにおいて、時間ステートチャートのAssume-Gurantee形式による演繹的詳細化検証手法を開発した。さらに、receptivenessの演繹的検証手法を実現した。
現在、以下の検討項目を研究中である:
1.時間ステートチャートのAssume-Gurantee形式による演繹的詳細化検証手法の実装及び実問題への適用。
2.分散システムのより高度なモデル化として、ハイブリッドオートマトンへの拡張。

  • 研究成果

    (5件)

すべて その他

すべて 文献書誌 (5件)

  • [文献書誌] 山根智,山ノ口崇: "実時間システムの演繹的検証と自動演繹的検証"情報処理学会研究報告MPS2000. 2000・29. 5-8 (2000)

  • [文献書誌] 山根智,山ノ口崇: "実時間システムの演繹的検証"電子情報通信学会研究報告SS2000. 2000・6. 1-8 (2000)

  • [文献書誌] 山根智,山ノ口崇: "AND構造とOR構造の分解による実時間ソフトウェアの安全性の演繹的検証"レクチャーノート(近代科学社). 25. 237-248 (2000)

  • [文献書誌] 山根智: "Assume-Gurantee検証による実時間システムの階層的設計支援手法"情報処理学会論文誌. 41・12. 3352-3362 (2000)

  • [文献書誌] 山根智,山ノ口崇: "Assume-Guarantee形式による実時間ソフトウェアの演繹的詳細化検証手法"電子情報通信学会研究報告SS2000. 2000・31. 1-8 (2001)

URL: 

公開日: 2002-04-03   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi