A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and?Maude
A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and?Maude
复制标题
鸿沟
DOI：
10.1007/978-3-030-41418-4_4
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Ogata Kazuhiro
中科院分区：
文献类型：
--
作者：
Minh Do Canh;Ogata Kazuhiro
提出了一种新的并发程序测试技术。该技术基本上是一种基于规范的测试技术。对于一个形式规格说明和一个并发程序P，状态序列由P生成，并由S检查是否接受。我们假设S在Maude中指定，P在Java中实现。Java Pathfinder（JPF）和Maude分别用于从P生成状态序列和检查S是否接受这些状态序列。即使不使用JPF检查任何违反属性的行为，JPF也经常在只生成状态序列时遇到臭名昭著的状态空间爆炸。因此，我们提出了一种技术，以产生状态序列从P和检查，如果这样的状态序列被接受的分层方式。一些实验表明，所提出的技术减轻了状态空间爆炸的情况下，否则只有一个JPF实例不能满足。
The paper proposes a new testing technique for concurrent programs. The technique is basically a specification-based testing one. For a formal specificationSand a concurrent programP, state sequences are generated fromPand checked to be accepted byS. We suppose thatSis specified in Maude andPis implemented in Java. Java Pathfinder (JPF) and Maude are then used to generate state sequences fromPand to check if such state sequences are accepted byS, respectively. Even without checking any property violations with JPF, JPF often encounters the notorious state space explosion while only generating state sequences. Thus, we propose a technique to generate state sequences fromPand check if such state sequences are accepted bySin a stratified way. Some experiments demonstrate that the proposed technique mitigates the state space explosion instances from which otherwise only one JPF instance cannot suffice.