| 研究課題/領域番号 |
18K11432
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分61030:知能情報学関連
|
|---|
| 研究機関 | 名古屋工業大学 |
|---|
研究代表者 |
世木 博久 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2021-03-31
|
| 研究課題ステータス |
完了 (2020年度)
|
| 配分額 *注記 |
4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2020年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2019年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2018年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
|---|
| キーワード | プログラム推論 / パターン発見 / 形式概念分析 / 計算論理 / パターンマイニング / ルール発見 / 仕様マイニング / 探索・論理・推論アルゴリズム |
|---|
| 研究成果の概要 |
本研究では，リアクティブ・システムなどの無限に継続する状態を扱えるソフトウェアの正当性を検証するための方法論の確立に向けて，次のような3つの研究成果を得た．(1) プログラムの実行ログから構成される系列データ集合から再現ルール形式の仕様を発見するアルゴリズムについて，その効率化のためにルール形成処理を並列化する処理方式を実装した．(2) 先行研究の再現ルール発見アルゴリズムを再検討し，それを改善した新たなアルゴリズムを提案して，有効性を実験的に確認した．(3) バグのあるプログラムについて，その実行時トレース・データからバグの位置特定のための相関ルールを導出するアルゴリズムの設計した．
|
| 研究成果の学術的意義や社会的意義 |
プログラムやシステムの検証に必要な要素として，証明すべき仕様を導出する機能と，システム設計や実装の誤り(バグ)を効率的に発見する機能について，その実現アルゴリズムを提案し，検証システムを構築するための知見を蓄積した． これらの結果は，実応用に向けたソフトウェアの検証システムの実現に寄与する意義がある．
|
