Testing Multi-Threaded Applications Using Answer Set Programming
Testing Multi-Threaded Applications Using Answer Set Programming
复制标题
使用答案集编程测试多线程应用程序
DOI：
--
复制
发表时间：
2018
影响因子：
0.9
通讯作者：
A. Namin
中科院分区：
文献类型：
--
作者：
Xiaozhen Xue;Sima Siami‐Namini;A. Namin
我们介绍了一种在多线程应用程序中形式化地表示和指定竞争条件的技术。答案集编程（ASP）是一种基于逻辑的知识表示范式，用于形式化表达应用领域中通过推理获得的信念。问题的透明和表达性以及强大的非单调推理能力使ASP能够在多项式时间内抽象地表示和求解某类NP困难问题。我们使用ASP形式化地表示竞争条件，从而表示具有共享内存模型的多线程应用程序中经常出现的潜在数据竞争。然后，我们使用ASP生成所有可能的测试输入和线程交错，即调度，其执行将导致确定性地暴露线程交错失败。我们用一些中等大小的Java程序评估了所提出的技术，我们的实验结果证实，所提出的技术实际上可以以低误报率暴露多线程程序中的常见数据竞争。我们推测，除了生成执行顺序导致数据竞争的线程调度之外，ASP在基于约束的软件测试研究中还有其他几个应用程序，可以用来表达和解决类似的测试用例生成问题，其中约束在确定搜索的复杂性方面起着关键作用。
We introduce a technique to formally represent and specify race conditions in multithreaded applications. Answer set programming (ASP) is a logic-based knowledge representation paradigm to formally express belief acquired through reasoning in an application domain. The transparent and expressiveness representation of problems along with powerful non-monotonic reasoning power enable ASP to abstractly represent and solve some certain classes of NP hard problems in polynomial times. We use ASP to formally express race conditions and thus represent potential data races often occurred in multithreaded applications with shared memory models. We then use ASP to generate all possible test inputs and thread interleaving, i.e. scheduling, whose executions would result in deterministically exposing thread interleaving failures. We evaluated the proposed technique with some moderate sized Java programs, and our experimental results confirm that the proposed technique can practically expose common data races in multithreaded programs with low false positive rates. We conjecture that, in addition to generating threads scheduling whose execution order leads to the exposition of data races, ASP has several other applications in constraint-based software testing research and can be utilized to express and solve similar test case generation problems where constraints play a key role in determining the complexity of searches.