Specification-Based Testing of Concurrent Programs

基于规范的并发程序测试

• 批准号: 9804112
• 负责人: Richard Carver
• 金额: --
• 依托单位: George Mason University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1998
• 资助国家: 美国
• 起止时间: 1998-08-01 至 2002-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9804112&HistoricalAwards=false
• 关键词: Specification; Based; Testing; Concurrent; Programs

9804112 This research focuses on the development of specification-based testing techniques for concurrent programs. The techniques being investigated are a combination of model-based and constraint- based testing techniques. For a given finite-state machine M, model-checking tools are used to find a list of temporal logic constraints that are satisfied by M. The constraints explicitly characterize M's logical branching structure, which otherwise appears only implicitly in the states and transitions of the finite-state machine. Test sequences are selected to cover the logical branches identified by the constraints. The objective of this research is to develop a structural testing methodology for finite state machine specifications that is not based on covering every state or transition. Two methods for addressing the state explosion problem during model-based test generation are being investigated. The first method, called specification slicing, is used to partition a finite-state model into several smaller sub- models that are used for test generation. The second method is called compositional testing. During compositional testing, test coverage properties are established for sub-models and these properties automatically hold for the whole system. Whether these two methods can be used to avoid the costly construction of complete system models for test generation is being investigated.***

9804112本研究致力于开发基于规格说明的并发程序测试技术。正在研究的技术是基于模型的测试技术和基于约束的测试技术的组合。对于给定的有限状态机M，使用模型检测工具来找到M满足的时态逻辑约束的列表。这些约束显式地描述了M的逻辑分支结构，否则它只隐式地出现在有限状态机的状态和转换中。选择测试序列以覆盖由约束标识的逻辑分支。这项研究的目的是开发一种有限状态机规范的结构测试方法，而不是基于覆盖每个状态或转换。正在研究两种方法来解决基于模型的测试生成期间的状态爆炸问题。第一种方法称为规范切片，用于将有限状态模型划分为几个较小的子模型，用于测试生成。第二种方法被称为成分测试。在组合测试期间，为子模型建立测试覆盖属性，并且这些属性自动适用于整个系统。是否可以使用这两种方法来避免为测试生成而构建完整的系统模型的成本高昂的问题正在研究中。