| 研究課題/領域番号 |
15K15969
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
島川 昌也 東京工業大学, 情報理工学院, 助教 (00749161)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2019-03-31
|
| 研究課題ステータス |
完了 (2018年度)
|
| 配分額 *注記 |
3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
2017年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2016年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2015年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | リアクティブシステム仕様 / 実現可能性 / ω-オートマトン / ωオートマトン |
|---|
| 研究成果の概要 |
リアクティブシステム仕様の実現可能性に関する検証は，仕様記述において見過ごされがちな危険な状況に陥る可能性を検出することができるが，一般に煩雑で計算コストの高い処理を伴う．本研究では，リアクティブシステム仕様の実現可能性判定の高速化を目的として，以下の事項に取り組んだ．(1) 部分的にBDDを利用して効率的に実現可能性判定手続きを実装する手法（部分シンボリック技法と呼ぶ）を開発した．この手法の最大の特長は，非近似的な実現可能性判定にも適用できることである．(2) 実現可能性判定を行う際に用いるωオートマトンをon-the-flyに簡約する手法を開発した．
|
| 研究成果の学術的意義や社会的意義 |
本研究の意義は，リアクティブシステム仕様の非近似的な実現可能性判定の効率化に成功した点である．既存研究では，シンボリック技法を適用するために近似的なアプローチがとられていた．本研究では，部分シンボリック技法により非近似的な実現可能性判定手続きを効率的に実装する手法を提案し，実験により，近似的なアプローチに引けを取らない性能がでることを確認した．
|
