@inproceedings{KaufmannKPSW14-sdmerge,
  author    = {Petra Kaufmann and Martin Kronegger and Andreas Pfandler and Martina Seidl and Magdalena Widl},
  title     = {A SAT-Based Debugging Tool for State Machines and Sequence Diagrams},
  booktitle = {Proc.\ SLE 2014},
  editor    = {Beno{\^{\i}}t Combemale and David J. Pearce and Olivier Barais and Jurgen J. Vinju},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2014},
  note      = {Best Paper Award},
  pages     = {21--40},
  abstract  = {An effective way to model message exchange in complex settings is to use UML sequence diagrams in combination with state machine diagrams. A natural question that arises in this context is whether these two views are consistent, i.e., whether a desired or forbidden scenario modeled in the sequence diagram can be or cannot be executed by the state machines. In case of an inconsistency, a concrete communication trace of the state machines can give valuable information for debugging purposes on the model level. This trace either hints to a message in the sequence diagram where the communication between the state machines fails, or describes a concrete forbidden communication trace between the state machines. To detect and explain such inconsistencies, we propose a novel SAT-based formalization which can be solved automatically  by an off-the-shelf SAT solver. To this end, we present the formal and technical foundations needed for the SAT-encoding, and an implementation inside the Eclipse Modeling Framework (EMF). We evaluate the effectiveness of our approach using grammar-based fuzzing.}
}