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

制定系统间协调的正式规范和验证方法

基本信息

批准号：
22K11976
负责人：
高木智彦
金额：
$ 1.33万
依托单位：
Kagawa University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2022
资助国家：
日本
起止时间：
2022-04-01 至 2027-03-31
项目状态：
未结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22K11976/
关键词：
ソフトウェア工学ソフトウェアテスト

项目摘要

本研究は、ソフトウェアによって実現された複数のシステムの間の連携（システム間連携）に関する欠陥を仕様の段階で検出する手法を構築し、システム群が提供する機能の信頼性向上に寄与することを目的としている。本年度の成果は、主に以下の2点である。(1) システム間連携に関する期待される振る舞いを仕様として記述するために、EPNAT（Extended Place/Transition Net with Attributed Tokens；属性付きトークンをもつ拡張プレース/トランジションネット）を応用する方法を明らかにした。EPNATは、システムの状態遷移に着目して実行可能かつ抽象的な形式仕様を記述するモデリング言語（拡張状態遷移モデル）の一種で、研究代表者らの過去の研究において考案されたものである。システム間連携を含む小規模なシステム群に関する例題に対して、EPNATによる仕様（EPNATモデル）を試験的に構築した。(2) EPNATモデルを自動検証するための、モデル探索アルゴリズムや充分性評価基準を構築した。モデル探索アルゴリズムは、探索方向を無作為に選択するため効率がよいとはいえないが、指定された検証条件（システム群の仕様上満たされるべき条件）に対する違反を欠陥として検出できる。探索は、欠陥を検出するか充分性評価基準を満たすまで繰り返す。充分性評価基準は、システム間連携に関与するEPNATのモデル要素（グルー・トランジションなど）に着目して構築した。これらを評価用ツールに実装し、先述の例題に試験適用して有効性を議論した。

本研究旨在开发一种在规范阶段检测由软件实现的多个系统之间的协调（系统间协调）缺陷的方法，并为提高一组系统提供的功能的可靠性做出贡献。今年的成绩主要有以下两点。 (1) 我们阐明了如何应用 EPNAT（具有属性令牌的扩展位置/转换网络）来描述有关系统间协作的预期行为作为规范。 EPNAT 是一种建模语言（扩展状态转换模型），它描述可执行的抽象形式规范，重点关注系统状态转换，是在研究负责人过去的研究中设计的。我们针对一小组系统的示例问题（包括系统间协调）在试验的基础上构建了 EPNAT 规范（EPNAT 模型）。 (2)构建了自动验证EPNAT模型的模型搜索算法和充分性评估标准。尽管模型搜索算法由于随机选择搜索方向而效率不高，但它们可以将违反指定验证条件（根据系统组的规范必须满足的条件）检测为缺陷。重复搜索，直到检测到缺陷或满足充分性标准。充分性评估标准是通过关注涉及系统间协调的 EPNAT 模型元素（粘合转换等）来构建的。我们将这些实施到评估工具中，将它们应用于上述示例问题，并讨论了它们的有效性。