| 研究課題/領域番号 |
18K18028
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 拓殖大学 (2019-2022)
東京工業大学 (2018) |
|---|
研究代表者 |
島川 昌也 拓殖大学, 工学部, 准教授 (00749161)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2021年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2020年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2019年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2018年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | ωオートマトン / 仕様検証 / ω-オートマトン |
|---|
| 研究成果の概要 |
形式仕様検証は人力では見つけにくい欠陥を検出できるが，その計算コストは高い．本研究では，リアクティブシステム仕様の非制限的検証，つまり仕様の構文や検証性質を制限しない検証のコスト削減を目的として，以下に取り組んだ．(1)リアクティブシステム仕様の検証で基盤となるωオートマトンや無限ゲームの効率的な操作手法を提案した．具体的には，無限ゲームの簡約方法や，部分シンボリック技法を用いたωオートマトンや無限ゲームの各種操作の効率的な実装手法を提案した．(2) 提案したωオートマトンや無限ゲームの効率的な操作手法を基に仕様検証器を開発した．
|
| 研究成果の学術的意義や社会的意義 |
形式仕様の自動検証はその有効性は認識されているものの，計算コストの高さからごく小規模な対象にその適用は限られている．特にリアクティブシステム仕様の自動検証では，理論的基盤として用いられるωオートマトンや無限ゲームの処理が煩雑であることから，その問題は顕著である．本研究では，そのような計算コストの問題を緩和させるため，いくつかの効率化手法を提案した．その成果はリアクティブシステム仕様の自動検証のより大規模で実際的な対象への適用に寄与するものと考えている．
|
