University of Twente Student Theses
Symbolic Model Checking with Partitioned BDDs in Distributed Systems
Torbecke, Janina (2017) Symbolic Model Checking with Partitioned BDDs in Distributed Systems.
|
PDF
2MB |
| Abstract: | In symbolic model checking Binary Decision Diagrams (BDDs) are often used to represent states of a system in a compressed way. By using reachability analysis the system’s entire state space can be explored. However, even with symbolic representation models can grow exponentially during an analysis such that they do not fit in a single machine’s working memory. Both multi-core and distributed reachability algorithms exist, but the combination of both is still uncommon. In this work we present a design for multi-core distributed reachability analysis. Our work is based on the multi-core model checking tool Sylvan and combines this with a BDD partitioning approach. As network traffic is one of the bottlenecks that are often reported in distributed reachability designs, we tried to minimize communication between machines. Our benchmark results show that our current design does not fully utilize available hardware capacity, but nevertheless our implementation was able to achieve speedups up to 29 compared to a linear execution and up to 5.3 compared to an existing multi-core distributed analysis tool. |
| 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/73721 |
| 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