Symbolic Step Encodings for Object Based Communicating State Machines

Reference:

Jori Dubrovin, Tommi Junttila, and Keijo Heljanko. Symbolic step encodings for object based communicating state machines. In Gilles Barthe and Frank S. de Boer, editors, Proceedings of the 10th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), volume 5051 of Lecture Notes in Computer Science, pages 96–112. Springer, 2008.

Abstract:

In this work, novel symbolic step encodings of the transition relation for object based communicating state machines are presented. This class of systems is tailored to capture the essential data manipulation features of UML state machines when enriched with a Java-like object oriented action language. The main contribution of the work is the generalization of the exists-step semantics approach, which Rintanen has used for improving the efficiency of SAT based AI planning, to a much more complex class of systems. Furthermore, the approach is extended to employ a dynamic notion of independence. To evaluate the encodings, UML state machine models are automatically translated into NuSMV models and then symbolically model checked with NuSMV. Especially in bounded model checking (BMC), the exists-step semantics often significantly outperforms the traditional interleaving semantics without any substantial blowup in the BMC encoding as a SAT formula.

Keywords:

UML state machine, bounded model checking, step semantics, verification

Suggested BibTeX entry:

@inproceedings{DubJunHel:FMOODS08,
    author = {Jori Dubrovin and Tommi Junttila and Keijo Heljanko},
    booktitle = {Proceedings of the 10th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08)},
    editor = {Gilles Barthe and Frank S. de Boer},
    pages = {96--112},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Symbolic Step Encodings for Object Based Communicating State Machines},
    volume = {5051},
    year = {2008},
}