模型检验驱动的含未知组件系统黑盒测试算法
Model-checking Driven Black-box Testing Algorithms for Systems with Unspecified Components
摘要：
基于组件的软件开发对系统验证提出了严峻的挑战，因为外部获得的组件可能是系统故障的新来源。这个问题不能完全解决，无论是模型检验或传统的软件测试技术单独由于以下几个原因：1）外部获得的组件通常是未指定/部分指定; 2）它通常是很难建立一个充分的标准来测试一个组件; 3）组件可以用来动态升级系统。本文介绍了一种新的方法（称为{ \em模型检查驱动的黑盒测试}），它将模型检验与传统的黑盒软件测试相结合，以一种完整、可靠和自动的方式来解决这个问题。其思想是，相对于一些要求（表示在CTL或LTL）的系统，使用模型检验技术，以获得一个条件（表示在通信图）为一个未指定的组件，使系统满足的要求，如果该条件是由组件满足，并可以通过测试组件的测试用例生成的条件上的飞行。在本文中，我们提出模型检验驱动的黑盒测试算法来处理CTL和LTL的要求。我们还通过一些例子来说明这个想法。
英文摘要：
Component-based software development has posed a serious challenge to system verification since externally-obtained components could be a new source of system failures. This issue can not be completely solved by either model-checking or traditional software testing techniques alone due to several reasons: 1) externally obtained components are usually unspecified/partially specified; 2)it is generally difficult to establish an adequacy criteria for testing a component; 3)components may be used to dynamically upgrade a system. This paper introduces a new approach (called {\em model-checking driven black-box testing}) that combines model-checking with traditional black-box software testing to tackle the problem in a complete, sound, and automatic way. The idea is to, with respect to some requirement (expressed in CTL or LTL) about the system, use model-checking techniques to derive a condition (expressed in communication graphs) for an unspecified component such that the system satisfies the requirement iff the condition is satisfied by the component, and which can be established by testing the component with test cases generated from the condition on-the-fly. In this paper, we present model-checking driven black-box testing algorithms to handle both CTL and LTL requirements. We also illustrate the idea through some examples.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
