Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

11-2011

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.

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 26th IEEE/ACM International Conference On Automated Software Engineering, ASE 2011, Lawrence, Kansan, USA, November 6-12

First Page

633

Last Page

636

ISBN

9781457716393

Identifier

10.1109/ASE.2011.6100143

Publisher

IEEE

City or Country

Lawrence, Kansan

Additional URL

https://doi.org/10.1109/ASE.2011.6100143

Download

Share

COinS