Journal of Computer Science and Technology ›› 2022, Vol. 37 ›› Issue (1): 4-28.doi: 10.1007/s11390-021-1673-5

Special Issue: Software Systems; Theory and Algorithms

• Special Section on Software Systems 2021 • Previous Articles     Next Articles

Event-Based Semantics of UML 2.X Concurrent Sequence Diagrams for Formal Verification

Inès Mouakher1, Fatma Dhaou1, and J. Christian Attiogbé2        

  1. 1Faculty of Sciences of Tunis, University of Tunis El Manar, Tunis 1068, Tunisia
    2Institute of Technology, University of Nantes, Nantes 44 322, France
  • Received:2021-06-01 Revised:2021-11-08 Accepted:2021-11-16 Online:2022-01-28 Published:2022-01-28
  • Contact: Inès Mouakher E-mail:ines.mouakher@fsegt.utm.tn
  • About author:Inès Mouakher received her Ph.D. degree in computer science from University of Nancy 2, France, in 2010. She joined University of Tunis El Manar, Tunis, as a lecture in 2004 and she became an assistant professor in computer science at University of Tunis El Manar in 2013. She is a member of the Laboratory of Computer Science Algorithmic and Heuristic Programming (LIPAH). Her research interests include formal methods, specification and verification, formal development (correction-by-construction), and distributed and concurrent system design. She published several peer-reviewed papers on these topics.

PDF (PC)

21

Supplement

1

UML 2.X sequence diagrams (SD) are among privileged scenarios-based approaches dealing with the complexity of modeling the behaviors of some current systems. However, there are several issues related to the standard semantics of UML 2.X SD proposed by the Object Management Group (OMG). They mainly concern ambiguities of the interpretation of SDs, and the computation of causal relations between events which is not specifically laid out. Moreover, SD is a semi-formal language, and it does not support the verification of the modeled system. This justifies the considerable number of research studies intending to define formal semantics of UML SDs. We proposed in our previous work semantics covering the most popular combined fragments (CF) of control-flow ALT, OPT, LOOP and SEQ, allowing to model alternative, optional, iterative and sequential behaviors respectively. The proposed semantics is based on partial order theory relations that permit the computation of the precedence relations between the events of an SD with nested CFs. We also addressed the issue of the evaluation of the interaction constraint (guard) for guarded CFs, and the related synchronization issue. In this paper, we first extend our semantics, proposed in our previous work; indeed, we propose new rules for the computation of causal relations for SD with PAR and STRICT CFs (dedicated to modeling concurrent and strict behaviors respectively) as well as their nesting. Then, we propose a transformational semantics in Event-B. Our modeling approach emphasizes computation of causal relations, guard handling and transformational semantics into Event-B. The transformation of UML 2.X SD into the formal method Event-B allows us to perform several kinds of verification including simulation, trace acceptance, verification of properties, and verification of refinement relation between SDs.

Key words: UML 2.X sequence diagram; formal semantics; nested combined fragment; partial order theory; Event-B;

[1] Micskei Z, Waeselynck H. The many meanings of UML 2 sequence diagrams: A survey. <i>Software & Systems Modeling</i>, 2011, 10(4): 489-514. DOI: 10.1007/s10270-010-0157-9.
<br>[2] Pickin S, Jézéquel J M. Using UML sequence diagrams as the basis for a formal test description language. In <i>Proc. the 4th International Conference on Integrated Formal Methods</i>, April 2004, pp.481-500. DOI: 10.1007/978-3-540-24756-2_26.
<br>[3] Störrle H. Trace semantics of interactions in UML 2.0. <i>J. Visual Languages and Computing</i>, 2004.
<br>[4] Lund M S. Operational analysis of sequence diagram specifications [Ph.D. Thesis]. University of Oslo, 2008.
<br>[5] André P, Rivière N, Waeselynck H. A Toolset for mobile systems testing. In <i>Proc. the 11th International Conference on Verification and Evaluation of Computer and Communication Systems</i>, August 2017, pp.124-138. DOI: 10.1007/978-3-319-66176-6_9.
<br>[6] Mahe E, Gaston C, Gall P L. Revisiting semantics of interactions for trace validity analysis. In <i>Proc. the 23rd International Conference on Fundamental Approaches to Software Engineering</i>, April 2020, pp.482-501. DOI: 10.1007/978-3-030-45234-6_24.
<br>[7] Dhaou F, Mouakher I, Attiogbé J C, Bsaies K. A causal semantics for UML 2.0 sequence diagrams with nested combined fragments. In <i>Proc. the 12th International Conference on Evaluation of Novel Approaches to Software Engineering</i>, April 2017, pp.28-29. DOI: 10.5220/0006314100470056.
<br>[8] Dhaou F, Mouakher I, Attiogbé J C, Bsaies K. An operational semantics of UML 2.X sequence diagrams for distributed systems. In <i>Proc. the 12th International Conference on Evaluation of Novel Approaches to Software Engineering</i>, April 2018, pp.158-182. DOI: 10.1007/978-3-319-94135-6_8.
<br>[9] Dhaou F, Mouakher I, Attiogbé J C, Bsaies K. Guard evaluation and synchronization issues in causal semantics for UML 2.X sequence diagrams. In <i>Proc. the 13th Int. Conference on Evaluation of Novel Approaches to Software Engineering</i>, March 2018, pp.275-282. DOI: 10.5220/0006708102750282.
<br>[10] Abrial J R. Modeling in Event-B---System and Software Engineering. Cambridge University Press, 2010.
<br>[11] Abrial J R, Butler M, Hallerstede S, Hoang T S, Mehta F, Voisin L. Rodin: An open toolset for modelling and reasoning in Event-B. <i>Int. J. Softw. Tools Technol. Transf.</i>, 2010, 12(6): 447-466. DOI: 10.1007/s10009-010-0145-y.
<br>[12] Leuschel M, Butler M. ProB: An Automated analysis toolset for the B Method. <i>Int. J. Softw. Tools Technol. Transf.</i>, Springer-Verlag, 2008, 10(2): 185-203. DOI: 10.1007/s10009-007-0063-9.
<br>[13] Boulanger J L. Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method. Wiley, 2014. DOI: 10.1002/9781119002727.
<br>[14] Rasch H, Wehrheim H. Checking the validity of scenarios in UML models. In <i>Proc. the 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems</i>, June 2005, pp.67-82. DOI: 10.1007/11494881_5.
<br>[15] Knapp A, Wuttke J. Model checking of UML 2.0 interactions. In <i>Proc. the Workshops and Symposia at 2016 International Conference on Model Driven Engineering Languages and Systems</i>, October 2007, pp.42-51. DOI: 10.1007/978-3-540-69489-2_6.
<br>[16] Lima V, Talhi C, Mouheb D, Debbabi M, Wang L, Pourzandi M. Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages. <i>Electron. Notes Theor. Comput. Sci.</i>, 2009, 254: 143-160. DOI: 10.1016/j.entcs.2009.09.064.
<br>[17] Cunha E, Custodio M, Rocha H, Barreto R. Formal verification of UML sequence diagrams in the embedded systems context. In <i>Proc. the 2011 Brazilian Symposium on Computing System Engineering</i>, November 2011, pp.39-45. DOI: 10.1109/SBESC.2011.18.
<br>[18] Zhu M, Wang H, Liu X, Han X. Formal analysis of sequence diagram with time constraints by model transformation. <i>Int. J. Softw. Informatics</i>, 2012, 6(2): 327-357.
<br>[19] Miyazaki H, Yokogawa T, Amasaki S, Asada K, Sato Y. Synthesis and refinement check of sequence diagrams. <i>IEICE Transactions on Information & Systems</i>, 2012, E95-D(9): 2193-2201. DOI: 10.1587/transinf.E95.D.2193.
<br>[20] Remenska D, Willemse T A C, Templon J, Verstoep K, Bal H E. Property specification made easy: Harnessing the power of model checking in UML designs. In <i>Proc. the 34th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems</i>, June 2014, pp.17-32. DOI: 10.1007/978-3-662-43613-4_2.
<br>[21] Muram F U, Tran H, Zdun U. Supporting automated containment checking of software behavioural models using model transformations and model checking. <i>Science of Computer Programming</i>, 2019, 174: 38-71. DOI: 10.1016/j.scico.2019.01.005.
<br>[22] Lima L, Miyazawa A, Cavalcanti A, Cornélio M, Iyoda J, Sampaio A, Hains R, Larkham A, Lewis V. An integrated semantics for reasoning about SysML design models using refinement. <i>Software & Systems Modeling</i>, 2017, 16(3): 875-902. DOI: 10.1007/s10270-015-0492-y.
<br>[23] Pan M, Chen S, Pei Y, Zhang T, Li X. Easy modelling and verification of unpredictable and preemptive interrupt-driven systems. In <i>Proc. the 41st IEEE/ACM International Conference on Software Engineering</i>, May 2019, pp.212-222. DOI: 10.1109/ICSE.2019.00037.
<br>[24] Chen X, Mallet F, Liu X. Formally verifying sequence diagrams for safety critical systems. In <i>Proc. the 14th Int. Symposium on Theoretical Aspects of Software Engineering</i>, December 2020, pp.217-224. DOI: 10.1109/TASE49443.2020.00037.
<br>[25] Alur R, Holzmann G J, Peled D. An analyzer for message sequence charts. In <i>Proc. the 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems</i>, March 1996, pp.35-48. DOI: 10.1007/3-540-61042-1_37.
<br>[26] Tahir O, Sibertin-Blanc C, Cardoso J. A causality-based semantics for UML sequence diagrams. In <i>Proc. IASTED Int. Conference on Software Engineering</i>, February 2005, pp.106-111.
<br>[27] Damchoom K, Butler M, Abrial J R. Modelling and proof of a tree-structured file system in Event-B and Rodin. In <i>Proc. the 10th International Conference on Formal Engineering Methods</i>, October 2008, pp.25-44. DOI: 10.1007/978-3-540-88194-0_5.
<br>[28] Mouakher I. Case study for sequence diagram transformation in Event-B. Technical Report, 2021.https://www.dropbox.com/s/8oeuy4gwfsa8cqh/mainTR.pdf?dl=0.
[1] De-Shuai Han, Qi-Liang Yang, Jian-Chun Xing, Guang-Lian Ma. EasyModel: A Refinement-Based Modeling and Verification Approach for Self-Adaptive Software [J]. Journal of Computer Science and Technology, 2020, 35(5): 1016-1046.
[2] Yu Zhou, Luciano Baresi, and Matteo Rossi. Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata [J]. , 2013, 28(1): 188-202.
[3] Cheng-Chun Shu, Hai-Yan Yu, and Hao-Zhi Liu. BEAP: An End-User Agile Programming Paradigm for Business Applications [J]. , 2006, 21(4): 609-619 .
[4] CHEN Chuanfeng (陈传峰), LI Zengzhi (李增智), TANG Yazhe (唐亚哲) and LIU Kangping (刘康平). Internet Network Resource Information Model [J]. , 2002, 17(6): 0-0.
[5] Xu Manwu; Lu Jianfeng; Zeng Fancong; Dai Jinwn;. A Formal Semantics for DAI Language NUML [J]. , 1995, 10(3): 227-238.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] . Online First Under Construction [J]. Journal of Computer Science and Technology, 0, (): 1 .
[2] Zhi-Neng Chen, Chong-Wah Ngo, Wei Zhang, Juan Cao, Yu-Gang Jiang. Name-Face Association in Web Videos: A Large-Scale Dataset, Baselines, and Open Issues[J]. , 2014, 29(5): 785 -798 .
[3] Fei Xia, De-Jun Jiang, Jin Xiong, Ning-Hui Sun. A Survey of Phase Change Memory Systems[J]. , 2015, 30(1): 121 -144 .
[4] André Brinkmann, Kathryn Mohror, Weikuan Yu, Philip Carns, Toni Cortes, Scott A. Klasky, Alberto Miranda, Franz-Josef Pfreundt, Robert B. Ross, Marc-André Vef. Ad Hoc File Systems for High-Performance Computing[J]. Journal of Computer Science and Technology, 2020, 35(1): 4 -26 .
[5] Yu-Tong Lu, Peng Cheng, Zhi-Guang Chen. Design and Implementation of the Tianhe-2 Data Storage and Management System[J]. Journal of Computer Science and Technology, 2020, 35(1): 27 -46 .
[6] Reza Jafari Ziarani, Reza Ravanmehr. Serendipity in Recommender Systems: A Systematic Literature Review[J]. Journal of Computer Science and Technology, 2021, 36(2): 375 -396 .
[7] Bo-Han Li, Yi Liu, An-Man Zhang, Wen-Huan Wang, Shuo Wan. A Survey on Blocking Technology of Entity Resolution[J]. Journal of Computer Science and Technology, 2020, 35(4): 769 -793 .
[8] Lie-Huang Zhu, Bao-Kun Zheng, Meng Shen, Feng Gao, Hong-Yu Li, Ke-Xin Shi. Data Security and Privacy in Bitcoin System: A Survey[J]. Journal of Computer Science and Technology, 2020, 35(4): 843 -862 .
[9] Dun Liang, Yuan-Chen Guo, Shao-Kui Zhang, Tai-Jiang Mu, Xiaolei Huang. Lane Detection: A Survey with New Results[J]. Journal of Computer Science and Technology, 2020, 35(3): 493 -505 .
[10] Lan Huang, Da-Lin Li, Kang-Ping Wang, Teng Gao, Adriano Tavares. A Survey on Performance Optimization of High-Level Synthesis Tools[J]. Journal of Computer Science and Technology, 2020, 35(3): 697 -720 .

ISSN 1000-9000(Print)

         1860-4749(Online)
CN 11-2296/TP

 Home
Editorial Board
Author Guidelines
Subscription		 Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
Tel.:86-10-62610746
E-mail: jcst@ict.ac.cn
 
  Copyright ©2015 JCST, All Rights Reserved