BROWSE
Detail
Conference Paper
Formal Verification of UML 2.0 Sequence Diagram
Cited - time in 
Share 
Share
- Authors
- Sa Choun Park, Tae Man Han, Gi Hwon Kwon
- Issue Date
- 2010-07
- Citation
- International Conference on Software Engineering and Knowledge Engineering (SEKE) 2010, pp.1-6
- Language
- English
- Type
- Conference Paper
- Abstract
- In UML 2.0, Sequence diagram is extended to have some reusable factors of interaction, e.g. combined fragment. But these additional features are hard to formally verify sequence diagrams. To overcome this obstacle, in this paper, we propose the formal semantics of sequence diagram with Finite State Process which is input language of LTS-BMC bounded model checker. The similarity between semantics of sequence diagram and FSP, interleaving and trace semantics, lead to formal verification of sequence diagram using a legacy welldeveloped bounded model checker.
- KSP Keywords
- Finite State, Formal semantics, Formal verification, Input language, Model checker, Sequence Diagram, UML 2.0, trace semantics