用于形式化验证的基于事件的UML 2.X并发时序图语义

doi:10.1007/s11390-021-1673-5

摘要: UMX 2.X时序图（SD）是一种基于情景以降低当前系统行为建模复杂度的方法。然而，有几个由对象管理组织（OMG）提出的UML 2.X SD的标准语义相关问题。这些问题主要体现在SDs解释的模糊性和事件因果关系的计算，该计算没有明确地呈现。此外，SD是一门半形式化语言，并且不支持所建模系统的验证。因此有大量定义UMLSDs形式化语义的相关研究。在我们之前的工作中所提出的语义，包括了最大众化的控制流的可替代、选择、循环和顺序组合片段（CF）以分别对可替代、选择、迭代和顺序行为进行建模；所提出的语义基于偏序理论关系，它可以计算含有嵌套CF的SD事件优先关系；此外，我们解决了被保护的CF的交互约束（guard）评价问题以及相关的同步问题。本文中，我们扩展了之前所提出的语义，为SD因果关系的计算提出了新的规则，它含有标准严格的CF（分别致力于并发和严格行为的建模）及其嵌套。接着，我们提出了基于Event-B的转换语义。我们建模方法强调计算因果关系、保护处理和用Event-B表示的转换语义。将UML 2.X SD转换为形式方法Event-B，使得我们可以实施包括仿真、轨迹验收、特性验证和SD细化关系的验证等多种验证工作。

关键词:

Abstract: UML 2.X sequence diagrams (SD) are among privileged scenarios-based approaches dealing with the complexityof modeling the behaviors of some current systems. However, there are several issues related to the standard semantics ofUML 2.X SD proposed by the Object Management Group (OMG). They mainly concern ambiguities of the interpretation ofSDs, and the computation of causal relations between events which is not specifically laid out. Moreover, SD is a semi-formallanguage, and it does not support the verification of the modeled system. This justifies the considerable number of researchstudies intending to define formal semantics of UML SDs. We proposed in our previous work semantics covering the mostpopular combined fragments (CF) of control-flow ALT, OPT, LOOP and SEQ, allowing to model alternative, optional, iterativeand sequential behaviors respectively. The proposed semantics is based on partial order theory relations that permit thecomputation of the precedence relations between the events of an SD with nested CFs. We also addressed the issue ofthe 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 causalrelations for SD with PAR and STRICT CFs (dedicated to modeling concurrent and strict behaviors respectively) as well astheir nesting. Then, we propose a transformational semantics in Event-B. Our modeling approach emphasizes computationof causal relations, guard handling and transformational semantics into Event-B. The transformation of UML 2.X SD into theformal method Event-B allows us to perform several kinds of verification including simulation, trace acceptance, verificationof properties, and verification of refinement relation between SDs.

Keywords:

[1] Micskei Z, Waeselynck H. The many meanings of UML 2 sequence diagrams: A survey. Software & Systems Modeling, 2011, 10(4): 489-514. DOI: 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. DOI: 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. DOI: 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. DOI: 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. DOI: 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. DOI: 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. DOI: 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. DOI: 10.1007/s10009-010-0145-y.
[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. DOI: 10.1007/s10009-007-0063-9.
[13] Boulanger J L. Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method. Wiley, 2014. DOI: 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. DOI: 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. DOI: 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. DOI: 10.1016/j.entcs.2009.09.064.
[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. DOI: 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.
[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. DOI: 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. DOI: 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. DOI: 10.1016/j.scico.2019.01.005.
[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. DOI: 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. DOI: 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. DOI: 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. DOI: 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. DOI: 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.

期刊类型引用(3)

1.	Runfang Wu, Ye Du, Yu Tang. A Research landscape on formal verification of UML dynamic modeling. The Journal of Supercomputing, 2025, 81(8) 必应学术
2.	Aissam Belghiat. Interleaving semantics and verification of UML 2 dynamic interactions using process algebra. Science of Computer Programming, 2025, 246: 103334. 必应学术
3.	Xiao-Ying Liu, Sheng-Rong Zou, Xue Geng, et al. Conversion of Timing Diagram to Event-B. 2023 8th International Conference on Computational Intelligence and Applications (ICCIA), 必应学术

其他类型引用(0)

其他相关附件

本文英文pdf
2022-1-2-1673-Highlights 点击下载(138KB)
本文附件外链
https://rdcu.be/cRabj