Sciweavers

Share
ICFEM
2009
Springer

Scalable Multi-core Model Checking Fairness Enhanced Systems

10 years 11 months ago
Scalable Multi-core Model Checking Fairness Enhanced Systems
Rapid development in hardware industry has brought the prevalence of multi-core systems with shared-memory, which enabled the speedup of various tasks by using parallel algorithms. The Linear Temporal Logic (LTL) model checking problem is one of the difficult problems to be parallelized or scaled up to multi-core. In this work, we propose an onthe-fly parallel model checking algorithm based on the Tarjan’s strongly connected components (SCC) detection algorithm. The approach can be applied to general LTL model checking or with different fairness assumptions. Further, it is orthogonal to state space reduction techniques like partial order reduction. We enhance our PAT model checker with the technique and show its usability via the automated verification of several real-life systems. Experimental results show that our approach is scalable, especially when a system search space contains many SCCs.
Yang Liu 0003, Jun Sun 0001, Jin Song Dong
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where ICFEM
Authors Yang Liu 0003, Jun Sun 0001, Jin Song Dong
Comments (0)
books