A Symbolic Model Checking Framework for Hierarchical Systems
BDD-based symbolic model checking is capable of verifying systems with a large number of states. In this paper, the authors report an extensible framework to facilitate symbolic encoding and checking of hierarchical systems. Firstly, a novel library of symbolic encoding functions for compositional operators (e.g., parallel composition, sequential composition, choice operator, etc.) are developed so that users can apply symbolic model checking techniques to hierarchical systems with little knowledge of symbolic encoding techniques (like BDD or CUDD). Secondly, as the library is language-independent, they build an extensible framework with various symbolic model checking algorithms so that the library can be easily applied to encode and verify different modeling languages.