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

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

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. ***