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. Technical Report B24, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2007.

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:

@techreport{HUT-TCS-B24,
    address = {Espoo, Finland},
    author = {Jori Dubrovin and Tommi Junttila and Keijo Heljanko},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {December},
    number = {B24},
    title = {Symbolic Step Encodings for Object Based Communicating State Machines},
    type = {Technical Report},
    year = {2007},
}