Name
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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/978-3-319-11245-9_2 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Sequence diagram,Programming language,Fuzz testing,Unified Modeling Language,Computer science,Boolean satisfiability problem,Theoretical computer science,Grammar,Finite-state machine,Eclipse,Debugging | Conference | 8706 |
ISSN | Citations | PageRank |
0302-9743 | 3 | 0.41 |
References | Authors | |
24 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Petra Kaufmann | 1 | 23 | 3.25 |
| Martin Kronegger | 2 | 53 | 4.64 |
| Andreas Pfandler | 3 | 95 | 10.98 |
| Martina Seidl | 4 | 685 | 51.78 |
| Magdalena Widl | 5 | 60 | 5.88 |