DICER 2.0: A New Model Checker for Data-Flow Errors of Concurrent Software Systems
DICER 2.0: A New Model Checker for Data-Flow Errors of Concurrent Software Systems
复制标题
DOI：
10.3390/math9090966
复制
发表时间：
2021
期刊：
影响因子：
2.4
通讯作者：
Dongming Xiang;Fang Zhao;Yaping Liu
中科院分区：
文献类型：
--
作者：
Dongming Xiang;Fang Zhao;Yaping Liu
Petri网被广泛用于并发软件系统的建模。目前，有许多不同类型的Petri网工具，可以分析系统的属性，如死锁，可达性和活性。然而，大多数工具不适合分析并发系统的数据流错误，因为它们没有形式化的数据信息，缺乏有效的计算方法来分析数据流。特别是当一个并发系统中有大量并发数据操作时，这些Petri网工具容易出现状态空间爆炸问题和伪状态。为了缓解这些问题，我们开发了一个新的模型检查器DICER 2.0。利用该工具，我们可以对并发软件系统的控制流和数据流进行建模。此外，基于展开技术可以检测数据不一致的错误，并可以通过守卫驱动的可达图（GRG）进行一些模型检查。最后通过实例分析和实验验证了该工具的有效性和优越性。
Petri nets are widely used to model concurrent software systems. Currently, there are many different kinds of Petri net tools that can analyze system properties such as deadlocks, reachability and liveness. However, most tools are not suitable to analyze data-flow errors of concurrent systems because they do not formalize data information and lack efficient computing methods for analyzing data-flows. Especially when a concurrent system has so many concurrent data operations, these Petri net tools easily suffer from the state–space explosion problem and pseudo-states. To alleviate these problems, we develop a new model checker DICER 2.0. By using this tool, we can model the control-flows and data-flows of concurrent software systems. Moreover, the errors of data inconsistency can be detected based on the unfolding techniques, and some model-checking can be done via the guard-driven reachability graph (GRG). Furthermore, some case studies and experiments are done to show the effectiveness and advantage of our tool.