next up previous
Next: Traversal Algorithms

Evaluating Symbolic Traversal Algorithms
Applied to Asynchronous Concurrent Systems

Marc Solé and Enric Pastor

Department of Computer Architecture
Technical University of Catalonia
08860 Castelldefels (Barcelona), Spain
{msole, enric}@ac.upc.es

Abstract:

The objective of this work is to show the special characteristics of asynchronous concurrent systems and motivate the necessity of developing specialized traversal algorithms for them. To fulfill this objective we will perform a comparative study between some of the most common existing traversal strategies and a number of strategies specially developed for asynchronous systems. A number of tools have been selected for that comparison. On one side NuSMV [1] and VIS [8], and on the other side TranSyT [7], a formal verification tool specialized for asynchronous systems. The results will highlight the importance of properly selecting the verification tool according to the type of system being analyzed. We will show that, in general, verification time can be greatly reduced, and in some cases specialized techniques will dictate the difference between enabling an efficient verification or collapsing the capabilities of the selected computer.




next up previous
Next: Traversal Algorithms
Enric Pastor 2004-05-28