@inproceedings{
    DubJunHel:FMOODS08,
    editor = "Barthe, Gilles and de Boer, Frank S.",
    author = "Dubrovin, Jori and Junttila, Tommi and Heljanko, Keijo",
    volume = "5051",
    publisher = "Springer",
    title = "Symbolic Step Encodings for Object Based Communicating State Machines",
    url = "http://www.tcs.hut.fi/~kepa/publications/",
    series = "Lecture Notes in Computer Science",
    booktitle = "Proceedings of the 10th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS 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.",
    responsibleauthor = "Dubrovin, Jori",
    opturl = "http://dx.doi.org/10.1007/978-3-540-68863-1_7",
    flags = "public SMUML DC",
    year = "2008",
    keywords = "UML state machine, bounded model checking, step semantics, verification",
    impactfactor = "D3",
    pages = "96--112"
}