| 研究課題/領域番号 |
12480075
|
|---|
| 研究機関 | 慶應義塾大学 |
|---|
研究代表者 |
岡田 光弘 慶応義塾大学, 文学部, 教授 (30224025)
|
|---|
| 研究分担者 |
米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)
林 晋 神戸大学, 工学部・情報知能工学科, 教授 (40156443)
小林 直樹 東京大学, 大学院・理学研究科, 専任講師 (00262155)
|
|---|
| キーワード | 線形論理 / 実時間システム / 形式仕様 / 形式検証 |
|---|
| 研究概要 |
線形論理を用いて並行計算システムの仕様・検証系を構築する試みはこれまでも成されてきたが、これらの成果を基にして、マルチ・エージェント並行計算実時間システムの仕様・検証系の理論を構築するとともに、我々の理論に基づく実時間システムの仕様・検証系のパイロット・インプレメンテーションを行った。
又、より本格的な実装のための研究を行った。我々の実時間システム仕様・検証系の特徴は、これまでの伝統的なモデルチェッキング法では捉えられなかった、実時間システム自身の動的変化を記述したり、そのような動的変化を伴う実時間並行計算システムに対する安全性をはじめとする種々の問題の検証を可能にした点にある.
|
