University of Twente Student Theses
Distributed Symbolic Reachability Analysis
Oortwijn, W.H.M (2015) Distributed Symbolic Reachability Analysis.
|
PDF
3MB |
| 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: | https://purl.utwente.nl/essays/67755 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page