Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

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

  • Regular Paper
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Micskei Z, Waeselynck H. The many meanings of UML 2 sequence diagrams: A survey. Software & Systems Modeling, 2011, 10(4): 489-514. https://doi.org/10.1007/s10270-010-0157-9.

  2. Pickin S, Jézéquel J M. Using UML sequence diagrams as the basis for a formal test description language. In Proc. the 4th International Conference on Integrated Formal Methods, April 2004, pp.481-500. https://doi.org/10.1007/978-3-540-24756-2_26.

  3. Störrle H. Trace semantics of interactions in UML 2.0. J. Visual Languages and Computing, 2004.

  4. Lund M S. Operational analysis of sequence diagram specifications [Ph.D. Thesis]. University of Oslo, 2008.

  5. André P, Rivière N,Waeselynck H. A Toolset for mobile systems testing. In Proc. the 11th International Conference on Verification and Evaluation of Computer and Communication Systems, August 2017, pp.124-138. https://doi.org/10.1007/978-3-319-66176-6_9.

  6. Mahe E, Gaston C, Gall P L. Revisiting semantics of interactions for trace validity analysis. In Proc. the 23rd International Conference on Fundamental Approaches to Software Engineering, April 2020, pp.482-501. https://doi.org/10.1007/978-3-030-45234-6_24.

  7. Dhaou F, Mouakher I, Attiogbé J C, Bsaies K. A causal semantics for UML 2.0 sequence diagrams with nested combined fragments. In Proc. the 12th International Conference on Evaluation of Novel Approaches to Software Engineering, April 2017, pp.28-29. https://doi.org/10.5220/0006314100470056.

  8. Dhaou F, Mouakher I, Attiogbé J C, Bsaies K. An operational semantics of UML 2.X sequence diagrams for distributed systems. In Proc. the 12th International Conference on Evaluation of Novel Approaches to Software Engineering, April 2018, pp.158-182. https://doi.org/10.1007/978-3-319-94135-6_8.

  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 Proc. the 13th Int. Conference on Evaluation of Novel Approaches to Software Engineering, March 2018, pp.275-282. https://doi.org/10.5220/0006708102750282

  10. Abrial J R. Modeling in Event-B—System and Software Engineering. Cambridge University Press, 2010.

  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. Int. J. Softw. Tools Technol. Transf., 2010, 12(6): 447-466. https://doi.org/10.1007/s10009-010-0145-y.

    Article  Google Scholar 

  12. Leuschel M, Butler M. ProB: An Automated analysis toolset for the B Method. Int. J. Softw. Tools Technol. Transf., Springer-Verlag, 2008, 10(2): 185-203. https://doi.org/10.1007/s10009-007-0063-9.

  13. Boulanger J L. Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method. Wiley, 2014. https://doi.org/10.1002/9781119002727.

  14. Rasch H, Wehrheim H. Checking the validity of scenarios in UML models. In Proc. the 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, June 2005, pp.67-82. https://doi.org/10.1007/11494881_5.

  15. Knapp A, Wuttke J. Model checking of UML 2.0 interactions. In Proc. the Workshops and Symposia at 2016 International Conference on Model Driven Engineering Languages and Systems, October 2007, pp.42-51. https://doi.org/10.1007/978-3-540-69489-2_6.

  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. Electron. Notes Theor. Comput. Sci., 2009, 254: 143-160. https://doi.org/10.1016/j.entcs.2009.09.064.

    Article  Google Scholar 

  17. Cunha E, Custodio M, Rocha H, Barreto R. Formal verification of UML sequence diagrams in the embedded systems context. In Proc. the 2011 Brazilian Symposium on Computing System Engineering, November 2011, pp.39-45. https://doi.org/10.1109/SBESC.2011.18.

  18. Zhu M, Wang H, Liu X, Han X. Formal analysis of sequence diagram with time constraints by model transformation. Int. J. Softw. Informatics, 2012, 6(2): 327-357.

    Google Scholar 

  19. Miyazaki H, Yokogawa T, Amasaki S, Asada K, Sato Y. Synthesis and refinement check of sequence diagrams. IEICE Transactions on Information & Systems, 2012, E95-D(9): 2193-2201. https://doi.org/10.1587/transinf.E95.D.2193.

  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 Proc. the 34th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, June 2014, pp.17-32. https://doi.org/10.1007/978-3-662-43613-4_2.

  21. Muram F U, Tran H, Zdun U. Supporting automated containment checking of software behavioural models using model transformations and model checking. Science of Computer Programming, 2019, 174: 38-71. https://doi.org/10.1016/j.scico.2019.01.005.

    Article  Google Scholar 

  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. Software & Systems Modeling, 2017, 16(3): 875-902. https://doi.org/10.1007/s10270-015-0492-y.

  23. Pan M, Chen S, Pei Y, Zhang T, Li X. Easy modelling and verification of unpredictable and preemptive interrupt-driven systems. In Proc. the 41st IEEE/ACM International Conference on Software Engineering, May 2019, pp.212-222. https://doi.org/10.1109/ICSE.2019.00037.

  24. Chen X, Mallet F, Liu X. Formally verifying sequence diagrams for safety critical systems. In Proc. the 14th Int. Symposium on Theoretical Aspects of Software Engineering, December 2020, pp.217-224. https://doi.org/10.1109/TASE49443.2020.00037.

  25. Alur R, Holzmann G J, Peled D. An analyzer for message sequence charts. In Proc. the 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems, March 1996, pp.35-48. https://doi.org/10.1007/3-540-61042-1_37.

  26. Tahir O, Sibertin-Blanc C, Cardoso J. A causality-based semantics for UML sequence diagrams. In Proc. IASTED Int. Conference on Software Engineering, February 2005, pp.106-111.

  27. Damchoom K, Butler M, Abrial J R. Modelling and proof of a tree-structured file system in Event-B and Rodin. In Proc. the 10th International Conference on Formal Engineering Methods, October 2008, pp.25-44. https://doi.org/10.1007/978-3-540-88194-0_5.

  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.

Download references

Author information

Authors and Affiliations

  1. Faculty of Sciences of Tunis, University of Tunis El Manar, 1068, Tunis, Tunisia

    Inès Mouakher & Fatma Dhaou

  2. Institute of Technology, University of Nantes, 44 322, Nantes, France

    J. Christian Attiogbé

Authors
  1. Inès Mouakher
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fatma Dhaou
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. J. Christian Attiogbé
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Inès Mouakher.

Supplementary Information

ESM 1

(PDF 138 kb)

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Mouakher, I., Dhaou, F. & Attiogbé, J.C. Event-Based Semantics of UML 2.X Concurrent Sequence Diagrams for Formal Verification. J. Comput. Sci. Technol. 37, 4–28 (2022). https://doi.org/10.1007/s11390-021-1673-5

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11390-021-1673-5

Keywords

Search

Navigation