A SAT-Based Debugging Tool for State Machines and Sequence Diagrams.
Lecture Notes in Computer Science(2014)
摘要
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.
更多查看译文
关键词
State Machine, Global State, Sequence Diagram, Eclipse Modeling Framework, Outgoing Transition
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要