Read, Write and Copy Dependencies for Symbolic Model Checking

Jeroen Meijer, Gijs Kant, Stefan Blom, Jan Cornelis van de Pol

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    15 Citations (Scopus)
    43 Downloads (Pure)

    Abstract

    This paper aims at improving symbolic model checking for explicit state modeling languages, e.g., Promela, Dve and mCRL2. The modular Pins architecture of LTSmin supports a notion of event locality, by merely indicating for each event on which variables it depends. However, one could distinguish four separate dependencies: read, may-write, must-write and copy. In this paper, we introduce these notions in a language-independent manner. In particular, models with arrays need to distinguish overwriting and copying of values. We also adapt the symbolic model checking algorithms to exploit the refined dependency information. We have implemented refined dependency matrices for Promela, Dve and mCRL2, in order to compare our new algorithms to the original version of LTSmin. The results show that the amount of successor computations and memory footprint are greatly reduced. Finally, the optimal variable ordering is also affected by the refined dependencies: We determined experimentally that variables with a read dependency should occur at a higher BDD level than variables with a write dependency.
    Original languageUndefined
    Title of host publicationProceedings of the 10th International Haifa Verification Conference, HVC 2014
    Place of PublicationBerlin
    PublisherSpringer
    Pages204-219
    Number of pages16
    ISBN (Print)978-3-319-13337-9
    DOIs
    Publication statusPublished - Nov 2014

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume8855
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Keywords

    • EWI-25296
    • METIS-309656
    • IR-93290

    Cite this