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

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

基本信息

批准号：
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のモデル要素（グルー・トランジションなど）に着目して構築した。これらを評価用ツールに実装し、先述の例題に試験適用して有効性を議論した。

这项研究旨在构建一种方法，用于检测软件在规范阶段实现的多个系统（Intersystem Collaporation）之间的缺陷，并有助于提高系统组提供的功能的可靠性。今年的结果主要如下：（1）我们已经澄清了如何应用EPNAT（具有归因于代币的扩展地点/过渡网）来描述与Intersystem协作有关的期望行为作为规格。 EPNAT是一种建模语言（扩展的状态过渡模型），它描述了可执行和抽象的形式规格，重点是系统状态过渡，并且是主要研究人员在先前的研究中设计的。构建了基于测试的规范（EPNAT模型），例如与包括系统间协作在内的小规模系统有关的问题。（2）已构建了模型搜索算法和充分评估标准，用于自动验证EPNAT模型。尽管模型搜索算法并不有效，因为它随机选择了搜索方向，但可以检测到对指定的验证条件（应在系统组的规格中应满足的条件）作为缺陷。重复搜索，直到检测到缺陷或满足足够评估标准为止。充分评估标准是通过关注EPNAT的模型元素（例如组过渡）来构建的，EPNAT涉及到系统间协作。这些是在评估工具中实施的，并对上述示例问题进行了测试，以讨论其有效性。