Sciweavers

Share
FMOODS
2008

Symbolic Step Encodings for Object Based Communicating State Machines

9 years 9 months ago
Symbolic Step Encodings for Object Based Communicating State Machines
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 -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 -step semantics often significantly outperforms the traditional interleaving semantics without any substantial blowup in the BMC encoding as a SAT formula.
Jori Dubrovin, Tommi A. Junttila, Keijo Heljanko
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2008
Where FMOODS
Authors Jori Dubrovin, Tommi A. Junttila, Keijo Heljanko
Comments (0)
books