実時間制約を考慮した開放型分散システムの形式化と階層的な設計手法
スポンサーリンク
概要
- 論文の詳細を見る
分散システムは大規模化して動作が複雑であり, 通信遅延などにより時間制約が重要である.その設計には次のような特徴がある.1.分散システムでは, プロセスが増減したり, プロセスの機能の変化が生じて, 各プロセスにとっては, 外部の環境の変化が激しい.このために, 自立性や発展性, すなわち, どのような外部環境であっても動作して, 機能拡充しやすい機構が必要である.2.分散システムは, 大規模かつ複雑さのために, 漸増的かつ階層的に, 抽象度の高い仕様から低い仕様を作成する必要がある.この場合, 抽象度の高い仕様と低い仕様との間の整合性を, どのような基準でどのような方法で保証するかが重要となる.3.分散システムでは, 通信遅延などによる時間制約が重量であり, 仕様記述や検証に時間制約を含める必要がある.4.設計手法の実用化には, 大規模なシステムを効率よく支援して, 設計者の負担が少ないことが重要である.本研究は, 次のように, 分散システムの発展性や自律性が記述できて検証できる設計方法論を提案することである.1.まず, 時間制約を含み, 発展性や自律性のあるプロセスが記述できる開放型時間オートマトンを形式的に定義する.2.次に, 分散システムの抽象度の高い仕様と低い仕様との間の整合性を時間模倣関係により保証して, 自律性を実時間記号モデル検査で保証する階層的な設計方法論を開発する.3.最後に, 上記方法論をアルゴリズム化して, Assume-Guarantee styleにより, 大規模システムの検証を可能とする.
- 一般社団法人電子情報通信学会の論文
- 1998-07-30
著者
関連論文
- CTL論理式と時間オートマトンに関する実時間記号モデル検査方式の提案
- 二分決定グラフによる実時間システムのモデルチェッキング検証
- 実時間制約を考慮した開放型分散システムの形式化と階層的な設計手法
- オートマトン理論に基づくリアルタイムソフトウェアの検証システム