| 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 2023)
|
| 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 |
本研究では、複数のソフトウェアシステムが連携する振る舞いを形式的モデルとして記述し、検証するための手法を開発している。ここでいう形式的モデルとは、コンピュータが解釈実行できるシステムの設計書のことである。本年度も、形式的モデルの言語としてEPNAT（Extended Place/transition Net with Attributed Tokens；属性付きトークンをもつ拡張プレース/トランジションネット）に着目した。制約条件（連携するシステム群が満たすべき条件）と検証基準（検証の充分性を判断するための基準）にしたがってモデルを探索し、システム間の連携に関する故障を設計段階で効果的に検出することが本研究の目的である。それには、EPNATで記述されたシステム群の設計モデルを、検証に適した検証用モデルに変換することが望ましい。そこで本年度は、VDM++（Vienna Development Methodで使用されるオブジェクト指向の形式的仕様記述言語）で記述され、VDMインタプリタ上で実行・検証することができる、EPNATのための検証用モデルについて検討した。この検証用モデルの特徴は、(1) システムの抽象的な現在状態を抽出する機能を有しているため、検証がより容易になると考えられること、(2) 設計モデルの構成要素をクラスとして定義しているため、可読性や保守性が改善されると考えられることである。検証用モデルの基本的なクラス構造などについて、例題に基づき議論した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
EPNATのための検証用モデルについて検討した成果をまとめ、国際会議で発表することができたため。
|
| Strategy for Future Research Activity |
引き続き、検証用モデルの探索アルゴリズムや検証基準の検討を進める。そして評価用ツールに実装して有効性を議論することを予定している。得られた研究成果については、国内研究集会や国際会議、論文誌などで発表することを予定している。
|
