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.

[img] PDF
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:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page