DICER 2.0: A New Model Checker for Data-Flow Errors of Concurrent Software Systems

Dongming Xiang, Fang Zhao and Yaping Liu
Additional contact information
Dongming Xiang: The School of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, China
Fang Zhao: The MoE Key Lab of Embedded System & Service Computing, Tongji University, Shanghai 201804, China
Yaping Liu: The School of Transportation Management, Zhejiang Institute of Communications, Hangzhou 310018, China

Mathematics, 2021, vol. 9, issue 9, 1-20

Abstract: 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.

Keywords: petri net; concurrent software systems; model-checking; data-flows (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2021
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/9/9/966/pdf (application/pdf)
https://www.mdpi.com/2227-7390/9/9/966/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:9:y:2021:i:9:p:966-:d:543342

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().