摘要
针对UML类图和序列图的一致性问题,在充分考虑了类继承关系、关联关系、类方法的可见性以及类方法的前、后置条件等因素对一致性影响的基础上,给出了判定类图和序列图一致性的必要条件和PVS元理论,提出了一种基于定理证明器PVS的一致性检验方法。在检验UML模型一致性时,把一致性检验问题转化为逻辑定理证明问题。实践表明,该方法对于提高UML模型的可信度,减少系统实现阶段的错误起到了一定作用。
The consistency checking between UML class diagrams and sequence diagrams is studied, and a PVS-based consistency checking approach is proposed. Firstly necessary conditions for deciding consistency is given and then the meta theory with PVS specification language is presented. To check consistency of UML model, the consistency checking is converted to a problem of theorem proving. Compared with other approaches, this technique involves more comprehensive factors, such as inheritance, associative relationship as well as visibility and pre-and post-conditions of class methods. It can mechanically analyze the consistency of UML model.
出处
《系统工程与电子技术》
EI
CSCD
北大核心
2004年第10期1481-1486,1525,共7页
Systems Engineering and Electronics
基金
高等学校博士学科点专项基金(K014010422)
"十五"国防预研项目基金(413150501)资助课题
关键词
统一建模语言
类图
序列图
机械定理
unified modeling language
class diagram
sequence diagram
mechanized theorem
