计算机科学技术学报 ›› 2022,Vol. 37 ›› Issue (1): 4-28.doi: 10.1007/s11390-021-1673-5

所属专题： Software Systems； Theory and Algorithms

• • 上一篇    下一篇

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

  

  • 收稿日期:2021-06-01 修回日期:2021-11-08 接受日期:2021-11-16 出版日期:2022-01-28 发布日期:2022-01-28

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

补充材料

1

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

关键词: UML 2.X时序图, 形式语义, 嵌套组合片段, 偏序理论, Event-B

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.

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. 一种逐步精化的自适应软件建模与验证方法[J]. 计算机科学技术学报, 2020, 35(5): 1016-1046.
[2] Yu Zhou, Luciano Baresi, Matteo Rossi. 基于层次式时间自动机的UML/MARTE状态机图的形式语义[J]. , 2013, 28(1): 188-202.
[3] . BEAP: 一种终端用户敏捷商业应用程序编程范型[J]. , 2006, 21(4): 609-619 .
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] . Online First Under Construction [J]. 计算机科学技术学报, 0, (): 1 .
[2] Zhi-Neng Chen, Chong-Wah Ngo, Wei Zhang, Juan Cao, Yu-Gang Jiang. 网络视频人脸—姓名关联：大规模数据库，基准实验和开放性问题[J]. , 2014, 29(5): 785 -798 .
[3] Fei Xia, De-Jun Jiang, Jin Xiong, Ning-Hui Sun. PCM内存系统研究综述[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. 高性能计算专用文件系统[J]. 计算机科学技术学报, 2020, 35(1): 4 -26 .
[5] Yu-Tong Lu, Peng Cheng, Zhi-Guang Chen. Tianhe-2数据存储与管理系统设计与实现[J]. 计算机科学技术学报, 2020, 35(1): 27 -46 .
[6] Reza Jafari Ziarani, Reza Ravanmehr. 推荐系统中的意外效应：系统文献综述[J]. 计算机科学技术学报, 2021, 36(2): 375 -396 .
[7] Bo-Han Li, Yi Liu, An-Man Zhang, Wen-Huan Wang, Shuo Wan. 实体消解中分块技术的综述[J]. 计算机科学技术学报, 2020, 35(4): 769 -793 .
[8] Lie-Huang Zhu, Bao-Kun Zheng, Meng Shen, Feng Gao, Hong-Yu Li, Ke-Xin Shi. 比特币系统的数据安全和隐私综述[J]. 计算机科学技术学报, 2020, 35(4): 843 -862 .
[9] 梁盾, 郭元晨, 张少魁, 穆太江, 黄晓蕾. 车道检测-新结果和调查研究[J]. 计算机科学技术学报, 2020, 35(3): 493 -505 .
[10] Lan Huang, Da-Lin Li, Kang-Ping Wang, Teng Gao, Adriano Tavares. 一个关于高级综合工具性能优化的综述[J]. 计算机科学技术学报, 2020, 35(3): 697 -720 .
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持：support@magtech.com.cn
总访问量：