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

• Material Type: 文書・図像類
• Title: 時相論理と並行計算、オートマトンの統合化による自律性のある分散システムの設計支援
• Author/Editor: 山根, 智; Yamane, Satoshi
• Author Heading: 山根, 智; Yamane, Satoshi
• Publication, Distribution, etc.: 金沢大学 理工研究域電子情報通信学系
• Publication Date: 2002-03
• Publication Date (W3CDTF): 2002-03
• Alternative Title: Design Support of Autonomous Distributed Systems by Integratig Temporal Logic, Concurrency Theny, Autom
• Periodical title: 平成13(2001)年度 科学研究費補助金 基盤研究(C) 研究成果報告書 = 2001 Fiscal Year Final Research Report
• No. or year of volume/issue: 1999-2001
• Volume: 1999-2001
• Pages: 110p.-
• Text Language Code: jpn
• Subject Heading: 開放型分散システム; 段階的詳細化; 詳細化検証; 時間オートマトン; ハイブリッドモデル; Assume-Guarantee; receptiveness; 仕様記述; open distributed systems; stepwise refinement; refinement verification; timed automata; hybrid models; receptioneness; specification
• Target Audience: 一般
• Note (General): 本研究では、従来個別に研究されていた形式的手法を統合化して、新しい分散システムの設計支援を実現するものである。そのポイントは、開放型システムとして分散システムをとらえて、実時間モデル及びハイブリッドモデルの観点からモデル化して、自動検証及び演縄的検証により設計の正当性を効率的に保証するものである。以上の観点より、我々は、以下の4つのモデルから、設計支援を実現した。(1)実時間型開放分散システムのAssume-guarantee方式による自動的設計支援:開放型分散システムの仕様記述言語として開放型時間オートマトンを形式化して、Assume-guarantee方式による時間模倣関係の自動検証及びreceptivenessの自動検証を実現した。これにより、実用レベルの分散システムの段階的詳細化設計が可能となった。(2)実時間型開放分散システムの演繹的設計支援:開放型分散システムの仕様記述言語として時間ステートチャートを形式化して、演繹的な詳細化検証の公理系を開発した。これにより、無限状態を有する分散ソフトウェアの段階的詳細化設計が可能となった。(3)実時間型開放分散システムのAssume-guarantee方式による演繹的設計支援:開放型分散システムの仕様記述言語としてクロック遷移モジュールを形式化して、Assume-guarantee方式による演繹的な詳細化検証の公理系及びreceptivenessの演繹的検証を開発した。これにより、実用レベルの分散ソフトウェアの段階的詳細化設計が可能となった。(4)ハイブリッドモデルに基づく開放分散システムの設計支援:開放型分散システムの仕様記述言語としてフェーズ遷移モジュールを形式化して、演繹的な詳細化検証の公理系を開発した。これにより、制御法則を含む分散ソフトウェァの段階的詳細化設計が可能となった。今後の課題としては、以上の開発した手法を本格的に計算機に実装して、大規模問題への適用及びその評価がある。; In this study, we realize our new design support system of distributed systems by-integrating existing formal methods. We formalize distributed systems as open distributed systems by real-time models or hybrid models, and verify them by automatic or deductive methods. We have developed the following four methods :(1)Automatic design support of real-time open distributed systems by Assume-guararnee methods : We have developed open timed automata and realized automatic verification of timed simulation relations and receptiveness by Assume-guarantee styles. Using this method, we can develop real distributed systems based on stepwise refinements.(2) Deductive design support of real-time open distributed systems : We have developed timed stateoharts and realized deductive refinement verification methods. Using this method, we can develop distributed systems represented by infinite states systems based on stepwise refinements.(3) Deductive design support of real-time open distributed systems by Assume-guarantee methods : We have developed clocked transition modules and realized deductive refinement verification methods and receptiveness verification methods by Assume-guarantee methods. Using this method, we can develop real distributed systems based on stepwise refinements.(4) Deductive design support of hybrid open distributed systems : We have developed phase transition | modules and realized deductive refinement derification methods. Using this method, we can develop I distributed systems represented by control laws based on stepwise refinements.We are now implementing our proposed methods by theorem provers and applying it to large systems.; 研究課題/領域番号:11680360, 研究期間(年度):1999-2001; 出典：「時相論理と並行計算、オートマトンの統合化による自律性のある分散システムの設計支援」研究成果報告書 課題番号11680360(KAKEN：科学研究費助成事業データベース（国立情報学研究所）) 本文データは著者版報告書より作成
• DOI: 10.24517/00053966
• Access Restrictions: 限定公開
• Related Material: https://kaken.nii.ac.jp/search/?qm=70263506; https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-11680360/; https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-11680360/116803602001kenkyu_seika_hokoku_gaiyo/
• Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）; https://irdb.nii.ac.jp
• Original Data Provider (Database): 金沢大学 : 金沢大学学術情報リポジトリKURA