Computer Science ›› 2017, Vol. 44 ›› Issue (2): 17-30, 64.doi: 10.11896/j.issn.1002-137X.2017.02.002

Previous Articles     Next Articles

Survey on Formal Semantics of UML Sequence Diagram

GUO Yan-yan, ZHANG Nan and TONG Xiang-rong   

  • Online:2018-11-13 Published:2018-11-13

Abstract: Formal semantics of UML sequence diagrams is critical to express the dynamic interaction of software system accurately.Therefore,a well-formed sequence diagram is a prerequisite for the analysis and verification of UML model and an important guarantee to improve the reliability of software systems.In this paper,different methods used in UML sequence diagram’s semantics were summarized and compared based on the working mechanisms and pros&cons,respectively.Meanwhile,the special issues with respect to how to define the semantics of UML sequence diagram were discussed as well.Finally,some specific research topics and directions in this area were suggested and proposed.

Key words: Unified modeling language,Formal methods,Sequence diagram,Combined interaction fragments,Denotational semantics,Operational semantics

[1] Object Management Group.UML 2.4.1 Superstructure Specification[R/OL].[2011-08-06](2015-10-01). 2.4.1/ Superstructure/PDF.
[2] Object Management Group.UML 2.5[R/OL].[2015-03-01].http:// /spec/UML/2.5/PDF.
[3] EGYED A.Automatically Detecting and Tracking Inconsisten-cies in Software Design Models[J].IEEE transactions on software engineering,2011,7(2):188-203.
[4] MICSKEI Z,WAESELYNCK H.The many meanings of UML 2 Sequence Diagrams a survey [J].Software & Systems Mode-ling,2011,0(4):489-514.
[5] LUND M S,REFSDAL A,STLEN K.Semantics of UMLModels for Dynamic Behavior-A Survey of Different Approaches[C]∥Model-Based Engineering of Embedded Real-Time Systems,2010:77-103.
[6] STRRLE H.Semantics of interactions in UML 2.0[C]∥ IEEE Symposium on Human Centric Computing Languages and Environments.Washington:IEEE Computer Society.2003:129-136.
[7] KNAPP A,STRRLE H.Efficient Representation of TimedUML2 Interactions [M]∥System Analysis and Modeling:Mo-dels and Reusability.2014,8769:110-125.
[8] YSTEIN H,KNUT EILIF H, RAGNHILD KOBRO R,et al.STAIRS towards formal design with sequence diagrams [J].Software & Systems Modeling,2005,4(4):355-357.
[9] MASS SOLDAL L,KETIL S.A Fully General Operational Semantics for UML 2.0 Sequence Diagrams with Potential and Mandatory Choice[C]∥ International Conference on Formel Methods.Springer-Verlag.2006:199-204 .
[10] MASS SOLDAL L,STLEN K.Deriving Tests from UML 2.0 Sequence Diagrams with neg and assert [C]∥Proceedings of the 2006 International Workshop on Automation of Software Test,2006.New York:ACM,2006:22-28.
[11] REFSDAL A,RUNDE R K,STLEN K.Stepwise refinementof sequence diagrams with soft real-time constraints [J].Journal of Computer and System Sciences,2015,81(7):1221-1251.
[12] REFSDAL A.Specifying computer systems with probabilisticsequence diagrams [D].Oslo:University of Oslo,2008.
[13] RUNDE R K,REFSDAL A,STLEN K.Relating computersystems to sequence diagrams:the impact of under-specification and inherent nondeterminism [J].Formal Aspects of Computing,2013,25(2):159-187.
[14] CENGARLE M V.UML 2.0 Interactions:semantics and refinement:TUM-I0415 [R].Institut für Informatik:Technische Universitt München,2004.
[15] CENGARLE M V,KNAPP A.An Institution for UML 2.0 interactions,TUM-I0808 [R].Institut für Informatik:Technische Universitt München,2008.
[16] LU L J,KIM D K.Required Behavior of UML Sequence Dia-grams:Semantics and Refinement[C]∥IEEE International Conference of Engineering of Complex Computer Systems.Las Vegas:IEEE.2011:127-136.
[17] LU L J,KIM D K.Refinement Inference for Sequence Diagrams[M]∥SDFSEM 2013:Theory and Practice of Computer Science.Berlin Heidelberg,2013:432-444.
[18] LU L J,KIM D K.Required Behavior of Sequence Diagrams:Se-mantics and Conformance [J].ACM Transactions on Software Engineering and Methodology,2014,23(2):1-16.
[19] GU S S,CAI S B,LI S X.A formal semantics for interactions in UML2 [J].Journal of Frontiers of Computer S-cience and Technology,2012,6(7):631-643.(in Chinese) 古思山,蔡树彬,李师贤.一种UML2 的交互的形式化语义 [J].计算机科学与探索,2012,6(7):631-643.
[20] SHEN H,ROBINSON M,NIU J W.A Logical Framework for Sequence Diagram with Combined Fragments,CS-TR-2011-015 [R].Austin:University of Texas at San Antonio,2011.
[21] SHEN H,ROBINSON M,NIN J W.Formal analysis of se-quence diagram with combined fragments[C]∥International Conference on Software Paradigm Trends.Nature Publishing Group.2012:44-54.
[22] SHEN H,KRISHNAN R,SLAVIN R,et al.Sequence Diagrams Aided Privacy Policy Specification[J].IEEE Transactions on Dependable and Secure Computing,2014(99):1-14.
[23] SUN M,BARBOSA L S.A coalgebraic semantic framework for reasoning about UML sequence diagram[C]∥ The 8th International Conference on Quality Software.Oxford:IEEE,2008:17-26.
[25] FILIPE J K.Modelling concurrent interactions [J].Theoretical Computer Science,2014,1(351):203-220 .
[26] FILIPE J K.Decomposing interactions[J].Algebraic Methodo-logy and Software Technology,2006,4019:189-203.
[27] HAMMAL Y.Branching Time Semantics for UML 2.0 Se-quence Diagrams[C]∥Formal Techniques for Networked and Distributed Systems(FORTE 2006).2006:259-274.
[28] HAMMAL Y.A Formal Methodology for Semantics and Time Consistency Checking of UML Dynamic Diagrams[J].Journal of the Chinese Institute of Engineers,2011,34(2):197-211.
[29] CAVARRA A,KSTER-FILIPE J.Combining Sequence Dia-grams and OCL for liveness[J].Electronic Notes in Theoretical Computer Science,2005,115:19-38.
[30] CAVARRA A,KSTER-FILIPE J.Formalizing Liveness-En-riched Sequence Diagrams Using ASMs[M]∥ Abstract State Machines 2004 Advance in Theory and Practice.Springer Berlin Heidelberg,2004:62-77.
[31] HAREL D,KANTOR A.Modal Scenarios as Automata[M]∥Language,Culture,Computation.Computing-Theory and Technology.Springer Berlin Heidelberg,2014:156-167.
[32] HAREL D,MAOZ S.Assert and negate revisited:modal semantics for UML Sequence Diagrams [J].Software & Systems Modeling,2008,7(2):237-253.
[33] LI W R,WANG Z J,ZHANG P C.Formal Semantics of Universal Modal Sequence Diagram [J].Journal of Software,2011,22(4):659-675.(in Chinese) 李雯睿,王志坚,张鹏程.模态顺序图uMSD的形式语义[J].软件学报,2011,22(4):659-675.
[34] WANG Z J,LI W R,YANG G X,et al.Research on Verification of Web Service Composition Based on uMSD[J].Computer Science,2011,38(9):119-125.(in Chinese) 王志坚,李雯睿,杨种学,等.基于uMSD的Web服务组合验证方法研究[J].计算机科学,2011,38(9):119-125.
[35] ZHANG C,DUAN Z H,TIAN C.Specitication and verification of UML2.0 sequence diagram based on event deterministic finite automata [J].Journal of Software,2011,22(11):2625-2638.(in Chinese) 张琛,段振华,田聪.基于事件确定有限自动机的UML2.0序列图描述与验证[J].软件学报,2011,22(11):2625-2638.
[36] ZHANG C.Testing and Vefification Methods Based on UML2.0models [D].Xi’an:Xidian University,2012.(in Chinese) 张琛.基于UML2.0模型的测试与验证方法 [D].西安:西安电子科技大学,2012.
[37] ZHANG C,DUAN Z H.Test Case Generation Based on UML2.0 Models [J].Journal of Xi’an Jiaotong University,2011,45(8):18-23.(in Chinese) 张琛,段振华.应用UML2.0模型的测试用例生成方法[J].西安交通大学学报,2011,45(8):18-23.
[38] ZHANG C,DUAN Z H.A UML2.0-Based Software SafetyTesting Method [J].Journal of Wuhan University (Natural Science Edition),2010,56(2):165-169.(in Chinese) 张琛,段振华.基于UML2.0的软件安全测试方法[J].武汉大学学报(理学版),2010,56(2):165-169.
[39] GRNMO R,MLLER-PEDERSEN B.From UML 2 Sequence Diagrams to State Machines by Graph Transformation [J].Journal of Object Technology,2011,0(8):1-22 .
[40] GRNMO R,KROGDAHL S,M LLER-PEDERSEN B.A collection operator for graph transformation [J].Software & Systems Modeling,2013,12(1):121-144.
[41] GRNMO R,RUNDE R K,MLLER-PEDERSEN B.Conf-luence of aspects for sequence diagrams [J].Software & System Modeling,2013,12(4):789-824.
[42] MESSAOUDI N,CHAOUI A,BETTAZ M.An Operational Semantics for UML 2 Sequence Diagrams Supported by Model Transformations [J].Procedia Computer Science,2015,56(1):604-611.
[43] NIU J W,ATLEE J M,DAY N A.Template semantics for mo-del-based notations [J].IEEE Transactions on Software Engineering,2003,29(10):866-882.
[44] SHEN H,VIRANI A,NIU J W.Formalize UML 2 SequenceDiagrams[C]∥High Assurance Systems Engineering Sympo-sium.IEEE.2008:437-440.
[45] LUND M S,STLEN K.Deriving tests from UML 2.0 se-quence diagrams with neg and assert[C]∥Automation of Software Test,2006.New York:ACM,2006:22-28.
[46] MASS SOLDAL L.Escalator Tool,v.1.5.5 [J/OL].[2015-10].
[47] GROSU R,SMOLKA S A.Safety-liveness semantics for UML 2.0 Sequence Diagrams[C]∥Application of Concurrency to System Design,2005.Washington:IEEE Computer Society,2005:6-14.
[48] LI X S,LIU Z M,HE J F.A formal semantics of UML sequence diagram[C]∥Software Engineering Conference,2004.Austra-lian:IEEE,2004:168-177.
[49] LI X S A.Characterization of UML Diagrams and their Consistency[C]∥Engineering of Complex Computer Systems,2006.Washington:IEEE Computer Society,2006:67-76.
[50] LI D,LI X S,LIU Z M,et al.Automated transformations from UML behavior models to contracts[J].Science China Information Sciences,2014,57(12):1-17.
[51] TRIBASTONE M,GILMORE S.Automatic translation of UML sequence diagrams into PEPA models[C]∥Quantitative Eva-luation of Systems,2008.Washington:IEEE,2008:205-214.
[52] BOWLES J,KLOUL L.A Strongly Consistent Transformation from UML Interactions to PEPA Nets[C]∥Computational Science and Its Applications,2014.Berlin Heidelberg:Springer,2014:90-105.
[53] LI Q S,CHU H,CHEN P.The Formal Semantics of UML Sequence Diagram Based on Process Algebra [J].Computer Science,2004,31(4):173-175,3.(in Chinese) 李青山,褚华,陈平.基于进程代数的UML序列图的形式语义[J].计算机科学,2004,31(4):173-175,3.
[54] ZHAO Y F.The study on formal semantics of dynamic UML digrams [D].Shanghai:East China Normal University,201 0.(in Chinese) 赵也非.动态UML子图的形式语义研究[D].上海:华东师范大学,2010.
[55] QIAN C,YAN X F,ZHOU Y,et al.Model checking consistency of sequence diagram and state machine based on state reduction [J].Application Research of Computers,2014,1(5):1452-1455.(in Chinese) 钱成,燕雪峰,周勇,等.基于状态约简的顺序图和状态图一致性检测[J].计算机应用研究,2014,1(5):1452-1455.
[56] LIMAV,TALHI C,MOUHEB D,et al.Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages [J].Electronic Notes in Theoretical Computer Science,2009,254:143-160.
[57] YOUNSI N,AMIRAT A,MENASRIA A.From UML 2.0 Sequence Diagrams to PROMELA code by Graph Transformation Using AToM3 [J/OL].[2015-10-1]. /viewdoc/ summary?doi=
[58] ZHANG T.Research on formal verification methods of model of complicated information system[D].Harbin:Harbin Engi-neering University,2012.(in Chinese) 张涛.复杂信息系统模型的形式化验证方法研究[D].哈尔滨:哈尔滨工程大学,2012.
[59] CENGARLE M,KNAPP A.Operational semantics of UML 2.0 interactions,TUM-I0505[R].Institut für Informatik:Technische Universitat München,2005.
[60] GIRAULT C.系统工程Petri网[M].王生原,余鹏,霍金健,译.北京:电子工业出版社,2005.
[61] STAINES T S.Transforming UML Sequence Diagrams into Petri Nets [J].Journal of Communication and Computer,2013(10):72-81.
[62] BOUABANA-TEBIBEL T,RUBIN S H.An interleaving se-mantics for UML 2 interactions using Petri nets[J].Information Sciences.2013,232(5):276-293.
[63] BOUARIOUA M,CHAOUI A,ELMANSOURI R.From UMLSequence Diagrams to Labeled Generalized Stochastic Petri Net Models Using Graph Transformation[M]∥e-Technologies and Networks for Development.Springer Berlin Heidelberg,2011:318-328.
[64] YANG N H,YU H Q,SUN H,et al.Modeling UML sequence diagrams using extended Petri nets [J].Telecommunication Systems,2012,51(2/3):147-158.
[65] FARIA J P,PAIVA A C R.A toolset for conformance testing against UML sequence diagrams based on event-driven colored Petri nets [J].International Journal on Software Tools for Technology Transfer,2016,18(3):1-20 .
[66] TAN H B,YAO S Z,XU J J.Behavioral Consistency Analysis ofthe UML Parallel Structures [J].Natural Biotechnology,2004,2(9):1146-1149.
[67] OUARDANI A,ESTEBAN P,PALUDETTO M,et al.A Meta-modeling Approach for Sequence Diagrams to Petri Nets Transformation within the requirements validation process[J/OL].2006 [2015-10-1].
[68] GUO Y Y,LIU J L.Formalization for model Element of UML Statechart in RSL [J].Computer Science,2013,0(5):177-183,5.(in Chinese) 郭艳燕,刘惊雷.UML状态机模型元素的RSL形式化定义[J].计算机科学,2013,40(5):177-183,5.

No related articles found!
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75, 88 .
[2] XIA Qing-xun and ZHUANG Yi. Remote Attestation Mechanism Based on Locality Principle[J]. Computer Science, 2018, 45(4): 148 -151, 162 .
[3] LI Bai-shen, LI Ling-zhi, SUN Yong and ZHU Yan-qin. Intranet Defense Algorithm Based on Pseudo Boosting Decision Tree[J]. Computer Science, 2018, 45(4): 157 -162 .
[4] WANG Huan, ZHANG Yun-feng and ZHANG Yan. Rapid Decision Method for Repairing Sequence Based on CFDs[J]. Computer Science, 2018, 45(3): 311 -316 .
[5] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[6] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[7] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[8] LIU Qin. Study on Data Quality Based on Constraint in Computer Forensics[J]. Computer Science, 2018, 45(4): 169 -172 .
[9] ZHONG Fei and YANG Bin. License Plate Detection Based on Principal Component Analysis Network[J]. Computer Science, 2018, 45(3): 268 -273 .
[10] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99, 116 .