Parallel Specification-Based Testing for Concurrent Programs
Parallel Specification-Based Testing for Concurrent Programs
复制标题
并发程序的基于并行规范的测试
DOI：
10.1109/access.2022.3155629
复制
发表时间：
2022
期刊：
影响因子：
3.9
通讯作者：
Ogata Kazuhiro
中科院分区：
文献类型：
--
作者：
Canh Minh Do;Ogata Kazuhiro
提出了一种新的并发程序测试技术。该技术是一种基于规范的测试。对于正式规范和并发程序p，状态序列由p生成，并由y检查是否接受。我们假设sis是在Maude中指定的，而pi是在Java中实现的。然后使用Java Pathfinder （JPF）和Maude分别从mpand生成状态序列，以检查这些状态序列是否被ys接受。即使不使用JPF检查任何属性违规，JPF在仅生成状态序列时也经常遇到臭名昭著的状态空间爆炸。因此，我们提出了一种从mp生成状态序列的技术，并以分层的方式检查这些状态序列是否被syn接受。开发了一种工具来支持所建议的技术，该技术可以自然地并行处理。实验结果表明，该方法可以有效地缓解直接使用JPF无法实现的状态空间爆炸。
The paper proposes a new testing technique for concurrent programs. The technique is a specification-based testing. 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. A tool is developed to support the proposed technique that can be processed naturally in parallel. Some experiments demonstrate that the proposed technique mitigates the state space explosion, which cannot be achieved with the straightforward use of JPF.