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

Material type: 文書・図像類

Author: 山根, 智ほか

Publisher: 金沢大学理工研究域電子情報通信学系

Publication date: 2002-03

Material Format: Digital

Capacity, size, etc.: -

NDC: -

View All

Notes on use

Note (General)：: 本研究では、従来個別に研究されていた形式的手法を統合化して、新しい分散システムの設計支援を実現するものである。そのポイントは、開放型システムとして分散システムをとらえて、実時間モデル及びハイブリッドモデルの観点からモデル化して、自動検証及び演縄的検証により設計の正当性を効率的に保証するものである。以...

Related materials as well as pre- and post-revision versions

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/

Search by Bookstore

Holdings of Libraries in Japan

This page shows libraries in Japan other than the National Diet Library that hold the material.

List of Cooperating Institutions and Databases

Please contact your local library for information on how to use materials or whether it is possible to request materials from the holding libraries.

other

Kanazawa University Repository for Academic Resources
Digital
You can check the holdings of institutions and databases with which 学術機関リポジトリデータベース（IRDB）（機関リポジトリ） is linked at the site of 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）.
Kanazawa University Repository for Academic Resources

Search by Bookstore

Bibliographic Record

You can check the details of this material, its authority (keywords that refer to materials on the same subject, author's name, etc.), etc.

Digital

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
Source: https://kanazawa-u.repo.nii.ac.jp/?action=repository_action_common_download&item_id=47642&item_no=1&attribute_id=26&file_no=1
https://kanazawa-u.repo.nii.ac.jp/?action=repository_action_common_download&item_id=47642&item_no=1&attribute_id=26&file_no=1
Access Restrictions: 限定公開
Rights (production): CC BY-NC-ND
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