Title :
A cut-off approach for bounded verification of parameterized systems
Author :
Yang, Qiusong ; Li, Mingshu
Author_Institution :
Lab. for Internet Software Technol., Beijing, China
Abstract :
The features in multi-threaded programs, such as recursion, dynamic creation and communication, pose a great challenge to formal verification. A widely adopted strategy is to verify tentatively a system with a smaller size, by limiting the depth of recursion or the number of replicated processes, to find errors without ensuring the full correctness. The model checking of parameterized systems, a parametric infinite family of systems, is to decide if a property holds in every size instance. There has been a quest for finding cut-offs for the verification of parameterized systems. The basic idea is to find a cut-off on the number of replicated processes or on the maximum length of paths needed to prove a property, standing a chance of improving verification efficiency substantially if one can come up with small or modest cut-offs. In this paper, a novel approach, called Forward Bounded Reachability Analysis (FBRA), based upon the cut-off on the maximum lengths of paths is proposed for the verification of parameterized systems. Experimental results show that verification efficiency has been significantly improved as a result of the introduction of our new cut-offs.
Keywords :
formal verification; multi-threading; reachability analysis; FBRA; Forward Bounded Reachability Analysis; bounded verification; model checking; multi-threaded programs; parameterized systems; replicated processes; Automata; Indexes; Process control; Radiation detectors; Reachability analysis; Software; Vectors; bounded model checking; cut-off; parameterized system;
Conference_Titel :
Software Engineering, 2010 ACM/IEEE 32nd International Conference on
Conference_Location :
Cape Town
Print_ISBN :
978-1-60558-719-6
DOI :
10.1145/1806799.1806851