システム間連携に関する形式的仕様の記述および検証手法の開発

Research Project

Project/Area Number	22K11976
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Multi-year Fund
Section	一般
Review Section	Basic Section 60050:Software-related
Research Institution	Kagawa University
Principal Investigator	高木智彦香川大学, 創造工学部, 准教授 (70509124)
Project Period (FY)	2022-04-01 – 2027-03-31
Project Status	Granted (Fiscal Year 2022)
Budget Amount *help	¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000) Fiscal Year 2026: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000) Fiscal Year 2025: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000) Fiscal Year 2024: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000) Fiscal Year 2023: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000) Fiscal Year 2022: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Keywords	ソフトウェア工学 / ソフトウェアテスト
Outline of Research at the Start	複数のシステムの連携によって高度化や合理化を図ろうとするなかで品質事故が多発している。この問題に対応するために、本研究では、Model-Driven Developmentを前提として、形式的仕様に拡張状態遷移モデルを採用し、次のi～iiiに取り組む。(i) システム間連携を検証するためのモデルの構築手法を開発する。(ii) システム間連携に関する制約条件の記述手法を開発する。(iii) 制約条件に違反しないことをモデル上で体系的に検証し、欠陥の発見を支援する手法を開発する。
Outline of Annual Research Achievements	本研究は、ソフトウェアによって実現された複数のシステムの間の連携（システム間連携）に関する欠陥を仕様の段階で検出する手法を構築し、システム群が提供する機能の信頼性向上に寄与することを目的としている。本年度の成果は、主に以下の2点である。 (1) システム間連携に関する期待される振る舞いを仕様として記述するために、EPNAT（Extended Place/Transition Net with Attributed Tokens；属性付きトークンをもつ拡張プレース/トランジションネット）を応用する方法を明らかにした。EPNATは、システムの状態遷移に着目して実行可能かつ抽象的な形式仕様を記述するモデリング言語（拡張状態遷移モデル）の一種で、研究代表者らの過去の研究において考案されたものである。システム間連携を含む小規模なシステム群に関する例題に対して、EPNATによる仕様（EPNATモデル）を試験的に構築した。 (2) EPNATモデルを自動検証するための、モデル探索アルゴリズムや充分性評価基準を構築した。モデル探索アルゴリズムは、探索方向を無作為に選択するため効率がよいとはいえないが、指定された検証条件（システム群の仕様上満たされるべき条件）に対する違反を欠陥として検出できる。探索は、欠陥を検出するか充分性評価基準を満たすまで繰り返す。充分性評価基準は、システム間連携に関与するEPNATのモデル要素（グルー・トランジションなど）に着目して構築した。これらを評価用ツールに実装し、先述の例題に試験適用して有効性を議論した。
Current Status of Research Progress	Current Status of Research Progress 2: Research has progressed on the whole more than it was originally planned. Reason (1) システム間連携に関する期待される振る舞いを仕様として記述するために、EPNATを応用する方法を明らかにするとともに、(2) EPNATモデルを自動検証するための、モデル探索アルゴリズムや充分性評価基準を構築することができたため。さらに、(1)(2)について成果をまとめ、国際会議で発表することができたため。
Strategy for Future Research Activity	モデル探索アルゴリズムや充分性評価基準を拡張すること、そしてそれらを評価用ツールに実装して有効性を議論することを予定している。必要に応じて、モデリング言語の拡張や他のモデリング言語の導入も検討する。得られた研究成果については、国内研究集会や国際会議、論文誌などで発表することを予定している。