| 研究課題/領域番号 |
16K00109
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 鶴見大学 |
|---|
研究代表者 |
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| 研究分担者 |
山本 光晴 千葉大学, 大学院理学研究院, 教授 (00291295)
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| 研究課題ステータス |
完了 (2018年度)
|
| 配分額 *注記 |
4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円)
2018年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2017年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2016年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
|---|
| キーワード | model checking / software / liveness / モデル検査 / Java / ソフトウェア / ソフトウェア検証 / アルゴリズム / ソフトウエア学 / 仕様記述・検証 |
|---|
| 研究成果の概要 |
モデル検査技術を用いてソフトウェアが正しく動作することを検証する「ソフトウェアモデル検査」において活性性質の検証に関して研究を行った．LTL論理式から作成されるBuchiオートマトンと状態空間の同期積を探索する際に，同一の状態を何度も作成するために遷移に大きなコストがかかるという点に着目し，同一状態を再利用することで平均的な実行時間を短くする方式を考案し，Java Pathfinderの上での実装を得た．
|
| 研究成果の学術的意義や社会的意義 |
ソフトウェアモデル検査は，安全性性質の検証には多くの場面で用いられており，プログラムの誤りを見つけることに役立っている．しかし，活性性質の検証事例は比較的少数である．この理由のひとつは性質記述の難しさ，もうひとつには計算量の大きさである．本研究は，Java Pathfinderというひとつのモデル検査器上での実装ではあるが，問題の後者の側面を改善するものである．
|
