| 研究課題/領域番号 |
22K11988
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 株式会社SRA(先端技術研究室) |
|---|
研究代表者 |
熊澤 努 株式会社SRA(先端技術研究室), 先端技術研究室, 研究員 (90847906)
|
|---|
| 研究分担者 |
滝本 宗宏 東京理科大学, 理工学部情報科学科, 教授 (00318205)
児玉 靖司 法政大学, 経営学部, 教授 (30266910)
神林 靖 日本工業大学, 先進工学部, 准教授 (40269527)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2022年度)
|
| 配分額 *注記 |
3,640千円 (直接経費: 2,800千円、間接経費: 840千円)
2024年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2023年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2022年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
|---|
| キーワード | モデル検査 / 粒子群最適化法 / 問題分割 / 目的関数 / 群知能 |
|---|
| 研究開始時の研究の概要 |
本研究では，ソフトウェアシステムを形式的に検証する技術の一手法であるモデル検査の高性能化と，検査結果の理解可能性の向上を目標として，複数の群れを用いた粒子群最適化法を用いた検査技法を開発する．複数の群れを効果的に活用するため，個々の群れが解く問題を小規模化する問題分割法を開発して実装する．次に，経験的知識を活用した検査の高性能化，軽量化技法を組込む．ベンチマークを使用して実装した検査技法を総合的に評価することで，その有効な検査問題と性質を明らかにする．
|
| 研究実績の概要 |
複数の群れが効率的に検査を進めるために，各群れが問題を小規模化する問題分割法を開発した．この問題分割法は，モデル検査において従来研究されてきた抽象化技術を活用する汎用的な方法であり，検査問題の性質に依存することなく使用できる利点がある．加えて，粒子群最適化法で使用する目的関数として，経験的知識に基づいて，検査の効率性と検査結果の読みやすさをバランス良く考慮した関数を開発した．この2つの技術を組込んだ複数の群れから成る粒子群最適化法のプロトタイプをPython言語で実装し，並行システムの検証問題をベンチマークとして性能評価を行った．評価の結果，従来法よりも軽量化，効率化が実現されたことを確認した．
以上の研究を遂行する中で，これまで認識していなかった2つの課題があることが明らかになった．第一の課題は，検査をどの程度網羅的に実施したかという網羅性を評価する必要があることである．古典的な検査法は決定的アルゴリズムを採用しており，網羅的に検査を行うことが保証されている．一方，本研究が扱う複数の群れを用いた粒子群最適化法による検査は，問題分割や経験的知識を活用することで，網羅性をある程度犠牲にして効率化を図る方法である．そのため，2022年度には，古典的な検査法との挙動の違いの理解と，更なる性能向上に向けた改善点の把握のために，網羅性を数値評価する指標を開発した．さらに，開発した検査法を反復実行することで網羅性を高める方法を開発した．第二の課題は，ベンチマークの開発の必要性である．検査法がどの程度汎用的に利用できるかを評価するには，広く知られているベンチマークだけではなく，多様なベンチマーク問題を対象にした評価実験が必要である．今後は，検査法の本格的な実装と性能改善に努めるとともに，ベンチマーク問題の作成課題にも取り組んでいきたいと考えている．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
2022年度は，1) 粒子群最適化法のソフトウェア工学領域での応用研究と，問題分割を利用した群知能の効率化研究に関する文献調査．2）性能評価のために必要なベンチマークの収集．3）複数の群れから成る粒子群最適化法を用いたモデル検査法の概要の整理，の3点の課題を遂行予定であった．
1) については，文献調査の結果，単一の群れだけから成る粒子群最適化法をモデル検査に適用した先行研究を拡張して，複数の群れを扱う方法を開発する方針で研究を進めることとした．
2）については，準備としてベンチマークに関する文献調査を行った結果，汎用的な検査法の開発と評価のためには，広く知られている問題をベンチマークとするだけでなく，多様なベンチマークで実験を行う必要があることが明らかになった．そのため，ベンチマークの収集に加えて，新たに検査問題を作成することが課題として得られた．
3)については，モデル検査で研究実績のある抽象化を用いることで，各群れが効率的に検査を進める方法を考案した．また，各群れが最適化する目的関数を考案し，Python言語で実装し手評価を行った。その結果，従来法を上回る性能を示すことを確認した．一方，以上の研究の結果，実施計画時には認識していなかった課題として，網羅性の評価が必要であることが分かった．この点については，問題分割を考慮した網羅性の評価指標と，開発した検査法を用いて網羅性を向上させる方法を考案した．考案した方法をPython言語で実装して，評価を行った．
以上から，2）と3）については，本プロジェクトで解決すべき新しい課題が研究中に判明したものの，モデル検査法を考案し，プロトタイプのPython言語での実装段階まで進めることができたため， おおむね順調に進展していると評価した．
|
| 今後の研究の推進方策 |
実装したモデル検査法の改良と，チューニングを進めていく予定である．新たな課題であるベンチマーク作成に関しては，作成に必要な課題を洗い出し自動化を検討する．必要に応じてPython言語で実装する．自動化については，モデル検査におけるベンチマーク生成の先行研究があり，その方法を用いることにより，本研究で必要とされるベンチマークの作成が可能な見込みである．作成したベンチマークを用いて，検査法の評価を行うことで，検査法の改良が効率的に進められるため，国際会議での成果発表を目指して研究を進めていきたいと考えている．
|
