具有自适应不确定性削减的定量验证
软件工程
2022-02-22 v2
摘要
随机模型被广泛用于验证系统是否满足其可靠性、性能及其他非功能需求。然而，验证的有效性取决于能否利用来自组件单元测试、监控、系统日志等的数据准确估计这些模型的参数。当可用数据不足时，模型受认知参数不确定性影响，验证结果不准确，基于此的任何工程决策可能无效。为解决这些问题，我们引入VERACITY，一种工具支持的迭代方法，用于在认知参数不确定性下高效且准确地验证非功能需求。VERACITY将置信区间定量验证与一种新的自适应不确定性削减启发式相结合，该启发式通过在一系列验证迭代中对特定系统组件进行单元测试来收集关于被验证模型参数的额外数据。VERACITY支持离散时间马尔可夫链的定量验证，基于包括模型对不同组件参数变化的敏感性以及单元测试各组件的开销（如时间或成本）等因素，决定每次迭代中测试哪些组件。我们通过将其用于基于远程协助服务系统与在线购物Web应用的非功能需求验证，展示了VERACITY的有效性与效率。
引用
@article{arxiv.2109.02984,
title = {Quantitative Verification with Adaptive Uncertainty Reduction},
author = {Naif Alasmari and Radu Calinescu and Colin Paterson and Raffaela Mirandola},
journal= {arXiv preprint arXiv:2109.02984},
year = {2022}
}