Title
An Automatic Approach to Model Checking UML State Machines
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 Zhang1564.71
Yang Liu2491116.11