UML序列图的操作语义及其在模型精化中的一致性检查
n Operational Semantics for UML Sequence Diagrams and Consistency Checking in Model Refinement
给UML赋予形式化的动态语义,就可以在需求、设计早期,对关键系统属性进行自动验证,进而保证软件质量,对软件开发设计起到指导作用。本文首先给出了UML序列图的基本构成元素和五种操作子的操作语义,提出了精确定义和pi演算转换规则,然后,以一个电话协议模型为例,给出了系统的UML序列图和状态图,并转换为pi演算代码,使用模型检测器,对系统的死锁性和互模拟等价性进行了自动验证,最后,在理论上对关键系统属性进行推理和演绎,给出了时间复杂度及其证明。本文提出的从UML序列图到pi演算的映射规则是双射的,可以应用于正向/逆向软件工程。
If UML is formalized with dynamic semantics, the key system properties can be automatically verified early in phase of requirement and design, which will guarantee software quality and play a guiding role for software design and development. First, we proposed the operational semantics for UML sequence diagrams comprised of basic elements and five fragment operators, as well as the exact definitions and translation rules to pi-calculus. Second, a telephone system is illustrated, the UML sequences diagrams and state diagrams of the system are presented and translated to pi-calculus. The properties of deadlocks and bi-simulation equivalence are automatically validated in model checker. Finally, the key system properties are manually reasoned and deduced in theory, as well as the complexity its proof. The mapping rules we proposed between UML sequence diagrams and pi-calculus are bi-direction, thus the theory can be applied in both forward and reverse software engineering.
刘强、杨宗源、赵也非、谢瑾奎
计算技术、计算机技术
UML序列图操作语义pi演算一致性检查软件确保
UML sequence diagramsOperational semanticspi-calculusonsistency checkingSoftware assurance
刘强,杨宗源,赵也非,谢瑾奎.UML序列图的操作语义及其在模型精化中的一致性检查[EB/OL].(2009-08-26)[2025-08-18].http://www.paper.edu.cn/releasepaper/content/200908-428.点此复制
评论