Traversal techniques for concurrent systems

Abstract

Symbolic model checking based on Binary Decision Diagrams (BDDs) is a verification tool that has received an increasing attention by the research community. Conventional breadth-first approach to state generation results is often responsible for inefficiencies due to the growth of the BDD sizes. This is specially true for concurrent systems in which existing research (mostly oriented to synchronous designs) is ineffective. In this paper we show that it is possible to improve BFS symbolic traverse for concurrent systems by scheduling the application of the transition relation. The scheduling scheme is devised analyzing the causality relations between the events that occur in the system. We apply the scheduled symbolic traverse to invariant checking. We present a number of schedule schemes and analyze its implementation and effectiveness in a prototype verification tool.