Please use this identifier to cite or link to this item:
|Title:||A symbolic model checking framework for hierarchical systems||Authors:||Nguyen, T.K.
|Issue Date:||2011||Citation:||Nguyen, T.K.,Sun, J.,Liu, Y.,Dong, J.S. (2011). A symbolic model checking framework for hierarchical systems. 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings : 633-636. ScholarBank@NUS Repository. https://doi.org/10.1109/ASE.2011.6100143||Abstract:||BDD-based symbolic model checking is capable of verifying systems with a large number of states. In this work, we 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, we 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. Lastly, the applicability and scalability of our framework are demonstrated by applying the framework in the development of symbolic model checkers for three modeling languages as well as a comparison with the NuSMV model checker. © 2011 IEEE.||Source Title:||2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings||URI:||http://scholarbank.nus.edu.sg/handle/10635/43171||ISBN:||9781457716393||DOI:||10.1109/ASE.2011.6100143|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.