Bridging the Gap between Enumerative and Symbolic Model Checkers

Stefan Blom, Jan Cornelis van de Pol, M. Weber

    Research output: Book/ReportReportProfessional

    86 Downloads (Pure)

    Abstract

    We present a method to perform symbolic state space generation for languages with existing enumerative state generators. The method is largely independent from the chosen modelling language. We validated this on three different types of languages and tools: state-based languages (PROMELA), action-based process algebras (muCRL, mCRL2), and discrete abstractions of ODEs (Maple). Only little information about the combinatorial structure of the underlying model checking problem need to be provided. The key enabling data structure is the "PINS" dependency matrix. Moreover, it can be provided gradually (more precise information yield better results). Second, in addition to symbolic reachability, the same PINS matrix contains enough information to enable new optimizations in state space generation (transition caching), again independent from the chosen modelling language. We have also based existing optimizations, like (recursive) state collapsing, on top of PINS and hint at how to support partial order reduction techniques. Third, PINS allows interfacing of existing state generators to, e.g., distributed reachability tools. Thus, besides the stated novelties, the method we propose also significantly reduces the complexity of building modular yet still efficient model checking tools. Our experiments show that we can match or even outperform existing tools by reusing their own state generators, which we have linked into an implementation of our ideas.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages8
    Publication statusPublished - 5 Jun 2009

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology
    No.TR-CTIT-09-30
    ISSN (Print)1381-3625

    Keywords

    • IR-67526
    • Model Checking
    • State Space Exploration
    • METIS-263921
    • EC Grant Agreement nr.: FP6/043235
    • EWI-15703
    • Symbolic reachability

    Cite this

    Blom, S., van de Pol, J. C., & Weber, M. (2009). Bridging the Gap between Enumerative and Symbolic Model Checkers. (CTIT Technical Report Series; No. TR-CTIT-09-30). Enschede: Centre for Telematics and Information Technology (CTIT).