分散システムのハイブリッドモジュールによる形式化と詳細化自動検証
スポンサーリンク
概要
- 論文の詳細を見る
本発表では, ハイブリッドシステムの仕様の一般的なモデルである, Alurらのハイブリッドモジュールを基礎として, 詳細化自動検証手法を提案する.ハイブリッドモジュールは, 時間モジュールの拡張であり, 温度や圧力といったより一般的な連続変数を扱うことが可能なモジュールである.なお, 提案する詳細化検証手法では, 状態空間の組み合わせ爆発を抑制するために, Assume-Guarantee形式による検証を実現する.この実現のためにハイブリッドモジュールのreceptivenessの自動検証を行う.さらに, 事例を用いて, 本提案手法の有効性を示す.
- 2001-11-15
著者
関連論文
- ペットロボットを用いた感情認識システム(人工知能, 認知科学)
- 離散確率分布を持つリアルタイムシステムの確率時間時相論理式の演繹的検証手法(検証/テストとデバッグ)
- 離散確率分布を持つリアルタイムシステムの確率時間双模倣関係と確率時同時相論理式の保存(設計手法)
- 離散確率分布を持つリアルタイムシステムの確率時間時相論理式の演繹的検証手法
- 離散確率分布を持つリアルタイムシステムの詳細化検証手法(検証/テストとデバッグ)
- 実時間システムのための近似手法に基づいた記号モデル検査器の開発と評価
- 離散確率分布を持つリアルタイムシステムの詳細化検証手法
- 東洋史研究のためのエージェントとサービス(「エージェント基礎」及び一般)
- 確率時間オートマトンの確率時間弱模倣検証理論(計算理論とアルゴリズムの新展開)
- 時間弱模倣関係と最悪応答時間に基づくリアルタイムソフトウェアの詳細化設計手法(2003年並列/分散/協調処理に関する「松江」サマーワークショップ(SWoPP松江2003))(DC-1高信頼化手法)
- 癒し設備実現のための感情認識システム (特集 福祉と設備管理)
- ハイブリッドシステムのモジュールの仕様記述と検証の手法
- ハイブリッドオートマトンによるリアルタイムソフトウェアの仕様記述とスケジューラビリティ検証
- ハイブリッドモジュールの詳細化自動検証手法
- ハイブリッドシステムの構成的証明とその計算機実験
- 分散システムのハイブリッドモジュールによる形式化と詳細化自動検証
- 離散確率分布を持つリアルタイムシステムの確率時間時相論理式の演繹的検証手法
- 時間オートマトンによるソフトリアルタイムシステムのスケジューリング解析(スケジューリング, VLSI 設計とテスト及び一般)