WEKO3
インデックスリンク
アイテム
時相論理と並行計算、オートマトンの統合化による自律性のある分散システムの設計支援
https://doi.org/10.24517/00053966
https://doi.org/10.24517/00053966ade66d9d-0dcc-4687-a522-145ec53b17ca
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
TE-PR-YAMANE-S-kaken 2002-110p.pdf (3.8 MB)
|
.png)
|
| Item type | 報告書 / Research Paper(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2019-05-13 | |||||
| タイトル | ||||||
| タイトル | 時相論理と並行計算、オートマトンの統合化による自律性のある分散システムの設計支援 | |||||
| タイトル | ||||||
| タイトル | Design Support of Autonomous Distributed Systems by Integratig Temporal Logic, Concurrency Theny, Autom | |||||
| 言語 | en | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18ws | |||||
| 資源タイプ | research report | |||||
| ID登録 | ||||||
| ID登録 | 10.24517/00053966 | |||||
| ID登録タイプ | JaLC | |||||
| 著者 |
山根, 智
× 山根, 智 |
|||||
| 書誌情報 |
平成13(2001)年度 科学研究費補助金 基盤研究(C) 研究成果報告書 en : 2001 Fiscal Year Final Research Report 巻 1999-2001, p. 110p., 発行日 2002-03 |
|||||
| 出版者 | ||||||
| 出版者 | 金沢大学 理工研究域電子情報通信学系 | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | 本研究では、従来個別に研究されていた形式的手法を統合化して、新しい分散システムの設計支援を実現するものである。そのポイントは、開放型システムとして分散システムをとらえて、実時間モデル及びハイブリッドモデルの観点からモデル化して、自動検証及び演縄的検証により設計の正当性を効率的に保証するものである。以上の観点より、我々は、以下の4つのモデルから、設計支援を実現した。 (1)実時間型開放分散システムのAssume-guarantee方式による自動的設計支援:開放型分散システムの仕様記述言語として開放型時間オートマトンを形式化して、Assume-guarantee方式による時間模倣関係の自動検証及びreceptivenessの自動検証を実現した。これにより、実用レベルの分散システムの段階的詳細化設計が可能となった。 (2)実時間型開放分散システムの演繹的設計支援:開放型分散システムの仕様記述言語として時間ステートチャートを形式化して、演繹的な詳細化検証の公理系を開発した。これにより、無限状態を有する分散ソフトウェアの段階的詳細化設計が可能となった。 (3)実時間型開放分散システムのAssume-guarantee方式による演繹的設計支援:開放型分散システムの仕様記述言語としてクロック遷移モジュールを形式化して、Assume-guarantee方式による演繹的な詳細化検証の公理系及びreceptivenessの演繹的検証を開発した。これにより、実用レベルの分散ソフトウェアの段階的詳細化設計が可能となった。 (4)ハイブリッドモデルに基づく開放分散システムの設計支援:開放型分散システムの仕様記述言語としてフェーズ遷移モジュールを形式化して、演繹的な詳細化検証の公理系を開発した。これにより、制御法則を含む分散ソフトウェァの段階的詳細化設計が可能となった。 今後の課題としては、以上の開発した手法を本格的に計算機に実装して、大規模問題への適用及びその評価がある。 |
|||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | 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. |
|||||
| 内容記述 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 研究課題/領域番号:11680360, 研究期間(年度):1999-2001 | |||||
| 内容記述 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 出典：「時相論理と並行計算、オートマトンの統合化による自律性のある分散システムの設計支援」研究成果報告書 課題番号11680360 (KAKEN：科学研究費助成事業データベース（国立情報学研究所）) 本文データは著者版報告書より作成 |
|||||
| 著者版フラグ | ||||||
| 出版タイプ | AM | |||||
| 出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa | |||||
| 関連URI | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | https://kaken.nii.ac.jp/search/?qm=70263506 | |||||
| 関連名称 | https://kaken.nii.ac.jp/search/?qm=70263506 | |||||
| 関連URI | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-11680360/ | |||||
| 関連名称 | https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-11680360/ | |||||
| 関連URI | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-11680360/116803602001kenkyu_seika_hokoku_gaiyo/ | |||||
| 関連名称 | https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-11680360/116803602001kenkyu_seika_hokoku_gaiyo/ | |||||
