Research Initiation Award: Specification-Based Testing and Analysis of Concurrent Software

研究启动奖：基于规范的并发软件测试与分析

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

9309043 Carver Specification-based development provides a rigorous and definitive basis for comparing the intended and actual behavior of a concurrent program. Nondeterministic behavior of concurrent programs creates the following problem during testing: when testing P with input X, a single execution is insufficient to determine the correctness of P with input X. Even if P with input X has been executed successfully many times, it is possible that a future execution of P with input X will produce an incorrect result. To deal with this problem, we force deterministic executions of P according to given synchronization sequences. Test sequences can be selected from P or from its specification. We will investigate how to derive constraints from specifications. Constraints derived from a specification can be compared with the actual constraints derived from source code in order to detect errors. Concurrent programs will be formally specified using process algebras and temporal logic. New techniques and tools will be incorporated into an existing validation environment to support both specification and program-based testing and analysis. ***

9309043基于Carver规范的开发为比较并发程序的预期行为和实际行为提供了严格而明确的基础。并发程序的不确定性行为在测试过程中产生了以下问题：当测试具有输入X的P时，单次执行不足以确定具有输入X的P的正确性。即使具有输入X的P已经被成功执行多次，将来具有输入X的P的执行也有可能产生错误的结果。为了解决这个问题，我们根据给定的同步序列强制执行P。测试序列可选自P或选自其规格。我们将研究如何从规范派生约束。可以将从规范派生的约束与从源代码派生的实际约束进行比较，以便检测错误。并发程序将使用进程代数和时序逻辑进行形式化说明。新的技术和工具将被纳入现有的验证环境，以支持基于规范和基于程序的测试和分析。***