Parameterized Reachability Graph for Software Model Checking Based on PDNet

Abstract

Model checking is a software automation verification technique. However, the complex execution process of concurrent software systems and the exhaustive search of state space make the model-checking technique limited by the state-explosion problem in real applications. Due to the uncertain input information (called system parameterization) in concurrent software systems, the state-explosion problem in model checking is exacerbated. To address the problem that reachability graphs of Petri net are difficult to construct and cannot be explored exhaustively due to system parameterization, this paper introduces parameterized variables into the program dependence net (a concurrent program model). Then, it proposes a parameterized reachability graph generation algorithm, including decision algorithms for verifying the properties. We implement LTL-x verification based on parameterized reachability graphs and solve the problem of difficulty constructing reachability graphs caused by uncertain inputs.