TY - GEN
T1 - Formal specification and automated verification of UML2.0 sequence diagrams
AU - Peng, Tu
AU - Ding, Gangyi
PY - 2012
Y1 - 2012
N2 - Software reliability is with critical importance in security demanding areas, including space exploration, e-business and military defense. UML sequence diagrams capture the collaborations of objects, and bridge the gap between abstract design and coding. Hence studying formal methods and automated verification of sequence diagram is indispensible to assure software reliability. In this paper, we establish formal specification rules for UML2.0 diagrams based on CCS, calculus of communicating system. Based on those rules, we propose specification algorithm and prove its linear complexity. Hence formal specifications of sequence diagrams can be obtained with programmed algorithm. In the end, we use a case study to illustrate our approach and show how automated verification can help designer discover design mistakes in UML2.0 sequence diagrams.
AB - Software reliability is with critical importance in security demanding areas, including space exploration, e-business and military defense. UML sequence diagrams capture the collaborations of objects, and bridge the gap between abstract design and coding. Hence studying formal methods and automated verification of sequence diagram is indispensible to assure software reliability. In this paper, we establish formal specification rules for UML2.0 diagrams based on CCS, calculus of communicating system. Based on those rules, we propose specification algorithm and prove its linear complexity. Hence formal specifications of sequence diagrams can be obtained with programmed algorithm. In the end, we use a case study to illustrate our approach and show how automated verification can help designer discover design mistakes in UML2.0 sequence diagrams.
KW - CCS
KW - UML sequence diagrams
KW - automated verification
KW - formal specification
KW - model checking
UR - http://www.scopus.com/inward/record.url?scp=84875028616&partnerID=8YFLogxK
U2 - 10.1109/GrC.2012.6468641
DO - 10.1109/GrC.2012.6468641
M3 - Conference contribution
AN - SCOPUS:84875028616
SN - 9781467323093
T3 - Proceedings - 2012 IEEE International Conference on Granular Computing, GrC 2012
SP - 370
EP - 375
BT - Proceedings - 2012 IEEE International Conference on Granular Computing, GrC 2012
T2 - 2012 IEEE International Conference on Granular Computing, GrC 2012
Y2 - 11 August 2012 through 13 August 2012
ER -