Abstract | ||
---|---|---|
UML has become the dominant modeling language in software engineering arena. In order to reduce cost induced by design issues, it is crucial to detect model-level errors in the initial phase of software development. In this paper, we focus on the formal verification of dynamic behavior of UML diagrams. We present an approach to automatically verifying models composed of UML state machines. Our approach is to translate UML models to the input language of our home grown model checker PAT in such a way as to be transparent for users. Compared to previous efforts, our approach supports a more complete subset of state machine including fork, join, history and submachine features. It alleviates the state explosion problem by limiting the use of auxiliary variables. Additionally, this approach allows to check safety/liveness properties (with various fairness assumptions), trace refinement relationships and so on with the help of PAT. |
Year | DOI | Venue |
---|---|---|
2010 | 10.1109/SSIRI-C.2010.11 | SSIRI (Companion) |
Keywords | Field | DocType |
uml state machine,finite state machines,uml diagram,model checker pat,automatic approach,model-level error,uml model,software development,state machine,modeling language,software engineering arena,trace refinement relationship,model checking,state explosion problem,input language,uml,model checking uml state,software fault tolerance,unified modeling language,uml state machines,pat,dominant modeling language,simulation languages,software engineering,formal verification,encoding,computational modeling,reliability engineering,history,programming,algorithms,synchronization,semantics,phase detection | Model checking,UML state machine,Programming language,UML tool,Unified Modeling Language,Computer science,Finite-state machine,Real-time computing,Applications of UML,Shlaer–Mellor method,Reliability engineering,Formal verification | Conference |
ISBN | Citations | PageRank |
978-1-4244-7644-2 | 16 | 0.74 |
References | Authors | |
13 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Shao Jie Zhang | 1 | 56 | 4.71 |
Yang Liu | 2 | 491 | 116.11 |