Symbolic Model Checking of Data-Intensive Systems

OData support
Molnár Vince
Department of Measurement and Information Systems

In safety critical software systems, the use of design-time verification, like model checking, is more and more common. As systems become more complex, the number of state variables of the systems also grows. This leads to the state space explosion problem in these ``data-intensive'' systems, where the state space cannot be stored with explicit methods.

To address this problem, symbolic model checking techniques were introduced. These methods store the state space with compact data structures, such as decision diagrams. Algorithms using decision diagrams can efficiently operate on and store huge state spaces.

The exploitation of the structure of the system model can lead to improvements in the storage of state spaces of complex systems consisting of several components. During the last several years, hierarchical set decision diagrams were introduced, which are naturally fitting to the hierarchical data structures of the models – reducing the size of the state space representation.

This thesis presents a theoretical overview and a new implementation of the set decision diagrams complete with operations and state space exploring algorithms. The approach is also compared to traditional symbolic methods found in the literature.


Please sign in to download the files of this thesis.