Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

12-2009

Abstract

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 on-the-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.

Keywords

Model Check, Parallel Algorithm, Linear Temporal Logic, Label Transition System, Strongly Connect Component

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12

First Page

426

Last Page

445

ISBN

9783642103728

Identifier

10.1007/978-3-642-10373-5_22

Publisher

Springer Link

City or Country

Rio de Janeiro, Brazil

Additional URL

https://doi.org/10.1007/978-3-642-10373-5_22

Download

Share

COinS