Skip to main content
placeholder image

Similarity-based search for model checking: a pilot study with java pathfinder

Conference Paper


Download full-text (Open Access)

Abstract


  • When a model checker cannot explore the entire

    state space because of limited resources, model checking becomes

    a kind of testing with an attempt to find a failure (violation of

    properties) quickly. We consider two state sequences in model

    checking: (i) the sequence in which new states are generated, and

    (ii) the sequence in which the states generated in sequence (i) are

    checked for property violation. We observe that neighboring

    states in sequence (i) often have similarities in certain ways.

    Based on this observation we propose a search strategy, which

    generates sequence (ii) in such a way that similar states are

    evenly spread over the sequence. As a result, neighboring states

    in sequence (ii) can have a higher diversity. A pilot empirical

    study with Java PathFinder suggests that the proposed strategy

    can outperform random search in terms of creating equal or

    smaller number of states to detect a failure.

Publication Date


  • 2013

Citation


  • Ibrahimov, E., Wang, J. & Zhou, Z. (2013). Similarity-based search for model checking: a pilot study with java pathfinder. 13th International Conference on Quality Software (pp. 238-244). China: IEEE.

Scopus Eid


  • 2-s2.0-84885572123

Ro Full-text Url


  • http://ro.uow.edu.au/cgi/viewcontent.cgi?article=2480&context=eispapers

Ro Metadata Url


  • http://ro.uow.edu.au/eispapers/1471

Start Page


  • 238

End Page


  • 244

Place Of Publication


  • China

Abstract


  • When a model checker cannot explore the entire

    state space because of limited resources, model checking becomes

    a kind of testing with an attempt to find a failure (violation of

    properties) quickly. We consider two state sequences in model

    checking: (i) the sequence in which new states are generated, and

    (ii) the sequence in which the states generated in sequence (i) are

    checked for property violation. We observe that neighboring

    states in sequence (i) often have similarities in certain ways.

    Based on this observation we propose a search strategy, which

    generates sequence (ii) in such a way that similar states are

    evenly spread over the sequence. As a result, neighboring states

    in sequence (ii) can have a higher diversity. A pilot empirical

    study with Java PathFinder suggests that the proposed strategy

    can outperform random search in terms of creating equal or

    smaller number of states to detect a failure.

Publication Date


  • 2013

Citation


  • Ibrahimov, E., Wang, J. & Zhou, Z. (2013). Similarity-based search for model checking: a pilot study with java pathfinder. 13th International Conference on Quality Software (pp. 238-244). China: IEEE.

Scopus Eid


  • 2-s2.0-84885572123

Ro Full-text Url


  • http://ro.uow.edu.au/cgi/viewcontent.cgi?article=2480&context=eispapers

Ro Metadata Url


  • http://ro.uow.edu.au/eispapers/1471

Start Page


  • 238

End Page


  • 244

Place Of Publication


  • China