Stochastic models are widely used to verify whether systems satisfy their reliability, performance and other nonfunctional requirements. However, the validity of the verification depends on how accurately the parameters of these models can be estimated using data from component unit testing, monitoring, system logs, etc. When insufficient data are available, the models are affected by epistemic parametric uncertainty, the verification results are inaccurate, and any engineering decisions based on them may be invalid. To address these problems, we introduce VERACITY, a tool-supported iterative approach for the efficient and accurate verification of nonfunctional requirements under epistemic parameter uncertainty. VERACITY integrates confidence-interval quantitative verification with a new adaptive uncertainty reduction heuristic that collects additional data about the parameters of the verified model by unit-testing specific system components over a series of verification iterations. VERACITY supports the quantitative verification of discrete-time Markov chains, deciding which components are to be tested in each iteration based on factors that include the sensitivity of the model to variations in the parameters of different components, and the overheads (e.g., time or cost) of unit-testing each of these components. We show the effectiveness and efficiency of VERACITY by using it for the verification of the nonfunctional requirements of a tele-assistance service-based system and an online shopping web application.
翻译:为了解决这些问题,我们采用了VERACITY, 这是一种由工具支持的迭接方法,用于在集合参数不确定性下有效和准确地核查不起作用的要求。 ERVACity将信任与间定量核查与一种新的适应性不确定性减少超常性核查相结合,通过对一系列核查迭代进行单位测试,收集关于经核实的模型具体系统组成部分参数的额外数据。 VERACITY支持对离散时间的Markov链进行定量核查,根据不同部件参数参数的变化对模型的敏感性和基于不同参数参数的变化进行测试。