The paper develops novel bounded model checking techniques for labelled transition systems. The aim is to increase the efficiency of BMC by exploiting the inherent concurrency in the product of LTSs in order to cover more executions of the product within a given bound. This is done by considering a non-standard execution model, step executions, where multiple actions can take place simultaneously and where component LTSs are determinized on-the-fly, i.e., a component may be in a set of states in a step instead of in just one as in standard interleaving executions. Step executions can be further restricted to a subclass called process executions without loosing reachable states. For bounded model checking of reachability properties of the product of LTSs the paper presents translation schemes from LTSs to a constrained Boolean circuit such that satisfying valuations of the circuit correspond to step (process) executions of the product. The translation schemes have been implemented and some experimental comparisons performed. The results show that the bound needed for step and process executions is in most cases lower than in interleaving executions and that the running time of the model checker using process executions is smaller than using steps. Moreover, the performance compares favorably to a state-of-the-art interleaving BMC implementation in the NuSMV system.

@inproceedings{
    JusHelNie:BMC2003_ini,
    author = {Jussila, Toni and Heljanko, Keijo and Niemel{\"a}, Ilkka},
    publisher = "Elsevier",
    title = "{BMC} via On-the-Fly Determinization",
    url = "http://www.tcs.hut.fi/~kepa/publications/",
    series = "{ENTCS}",
    booktitle = "Proceedings of the first International Workshop on Bounded Model Checking",
    year = "2003",
    month = "July",
    volume = "89",
    flags = "copy,SA-53695",
    address = "Boulder, Colorado, USA",
    keywords = "bounded model checking",
    abstract = "The paper develops novel bounded model checking techniques for labelled transition systems. The aim is to increase the efficiency of BMC by exploiting the inherent concurrency in the product of LTSs in order to cover more executions of the product within a given bound. This is done by considering a non-standard execution model, step executions, where multiple actions can take place simultaneously and where component LTSs are determinized on-the-fly, i.e., a component may be in a set of states in a step instead of in just one as in standard interleaving executions. Step executions can be further restricted to a subclass called process executions without loosing reachable states. For bounded model checking of reachability properties of the product of LTSs the paper presents translation schemes from LTSs to a constrained Boolean circuit such that satisfying valuations of the circuit correspond to step (process) executions of the product. The translation schemes have been implemented and some experimental comparisons performed. The results show that the bound needed for step and process executions is in most cases lower than in interleaving executions and that the running time of the model checker using process executions is smaller than using steps. Moreover, the performance compares favorably to a state-of-the-art interleaving BMC implementation in the NuSMV system."
}

AUTHORS:

ABSTRACT:

URL:
http://www.tcs.hut.fi/~kepa/publications/

AUTHORS:

ABSTRACT:

URL: http://www.tcs.hut.fi/~kepa/publications/

URL:
http://www.tcs.hut.fi/~kepa/publications/