University of Twente Student Theses


Distributed Symbolic Reachability Analysis

Oortwijn, W.H.M (2015) Distributed Symbolic Reachability Analysis.

[img] PDF
Abstract:Model checking is an important tool in program verification. Model checkers generally examine the entire state space of a model to find behaviour that differs from a given formal specification. Most temporal safety properties can be verified via reachability analysis. A major limitation is the state space explosion problem, which occurs when the state space does not fit into the available memory. State spaces can efficiently be stored as Binary Decision Diagrams (BDDs), a data structure used to efficiently represent sets. The BDD representations of state spaces can then be manipulated via BDD operations, which enables symbolic reachability analysis. Moreover, more hardware resources can be employed, so that larger state spaces can be stored and processed in less time. Our research goal is to implement distributed BDD operations that scale efficiently along all processing units and memory connected via a high-performance network. We designed an RDMA-based distributed hash table and private deque work stealing algorithms. Both components are micro-benchmarked and used to implement the actual BDD operations. With respect to parallel symbolic reachability, by paying an acceptable performance price, the combined memory of a network of workstations can be used efficiently, and adding workstations does not decrease performance.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page