| 研究課題/領域番号 |
21K11826
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 信州大学 |
|---|
研究代表者 |
岡野 浩三 信州大学, 学術研究院工学系, 教授 (70252632)
|
|---|
| 研究分担者 |
岡本 圭史 仙台高等専門学校, 総合工学科, 教授 (00308214)
関澤 俊弦 日本大学, 工学部, 准教授 (10549314)
小形 真平 信州大学, 学術研究院工学系, 准教授 (10589279)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2022年度)
|
| 配分額 *注記 |
3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
2024年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2023年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2022年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2021年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
|---|
| キーワード | 機械学習 / 形態素解析 / 自然語処理 / 時間オートマトン / 有界モデル検査 / バグ局所化 / 自然語解析 / 反例解析 |
|---|
| 研究開始時の研究の概要 |
情報システムにおいては，開発期間の短縮化と高信頼性の担保の両立が大きな課題である．
情報システムの要求記述においては自然語仕様記述が行われている．また，要求解析についてはSTAMPに基づいた解析手法STPAに形式手法を併せる方法も有効であると考えられる．
本研究では，主に組込みシステムを対象に4年の計画で上記の研究を行い，提案手法や提案システムの有効性，とりわけ，自然語処理と形式手法の組み合わせによる安全性の検証に関する有効性を確認していく．
|
| 研究実績の概要 |
本研究では次の学術的問題を対象とする．(RQ1) 自然語による仕様記述から状態遷移モデルや検証性質等，形式的仕様記述へ適切に変換する方法論はあるのか?(RQ2) モデル検査の反例の有効活用はどこまでできるか? (RQ3) STAMP/STPA と自然言語処理，形式手法との連携方法は? 今年度は機械学習をもちいたソフトウェア開発、自然言語処理を用いた要求仕様解析、時間オートマトンのモデル検査ツールの開発の３点で大きく進展した。機械学習をもちいたソフトウェア開発ではJavaを対象にモデル検査の出力の可読性向上のを図る方法について成果をだした。また、ソフトウェアのバグ限定手法であるフォールトローカライゼーションを従来の通り、統計的指標を用いる方法ではなく、機械学習を応用する方法を改良することによって、より精度良く行う方法を考案し、研究会や国際会議で発表をおこなった。
要求仕様書の自然語解析を形態素解析と構文解析を組みわせて行い、状態遷移図作成に必要な要素を抽出する研究を精力的に行い、特にラムダカリキュラスを用いた時間関係推論を活用した方法論を考案し、複数の情報システムに活用し、国際会議で発表を行った。この研究成果をさらに発展させ、機械学習を活用した要求仕様の解析に取り組み始めている。
時間オートマトンを用いたモデル検査についてはSMT/SAT式に帰着する方法論をさらに一般時間オートマトンに拡張する方法を実装し、ツールとして実装することに成功した。この結果を国際会議に発表した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
2022年度は自然語要求仕様記述の解析において機械学習を援用した形態素解析を活用する方法や数理論理に基づく論理推論を活用し，精度を向上する方法について国際会議論文に発表するなどの成果をだした．具体的には，“Reducing Syntactic Complexity for Information Extraction from Japanese Requirement Specifications,” (APSEC 2022), “A Method for Matching Patterns Based on Event Semantics with Requirements,” (JCKBSE 2022) 等の国際会議で発表を行った．
コードのバグ解析については機械学習を援用することによるフォールト局在化について精度を上げる結果をだした．また，機械学習そのもの質の良さを議論する枠組みの基本的な成果を実験結果として示すことができた．これらは主に信学会の研究会で発表を行っている．また，機械学習を用いたフォールト局在化については複数のアプロ―チを研究しており，バーチャルテストケース実行による局所化については “Improve Measuring Suspiciousness of Bugs in Spectrum-Based Fault Localization With Deep Learning,” IWIN2022にて発表を行った．
また，時間オートマトンに対する有界モデル検査の手法を実装した結果について“A Bounded Model Checker for Timed Automata and Its Application to LTL Properties” KES2022で発表することができた．多くの点で研究が順調に進んでいるといえる．
|
| 今後の研究の推進方策 |
今後は引き続き自然語要求仕様記述の解析の研究を進めるとともに，コードのバグ解析については機械学習を援用する方法についてさらに取り組んでいきたい，また，実装した時間オートマトンに対する有界モデル検査の手法を用いた反例を解析することによるバグ発見を機械学習に援用する方法について取り組みたい．また機械学習プログラムの安全性解析，セキュリティー保証を解析する方法についても取り組みたい．これらの成果を国内研究会，国際会議等に発表していきたい．
|
