基于PVS的UML类图和序列图的一致性检验  

PVS-based consistency checking for UML class diagrams and sequence diagrams

作　　者：刘晓健[1] 陈平[1] 

机构地区：[1]西安电子科技大学软件工程研究所,陕西西安710071

出　　处：《系统工程与电子技术》2004年第10期1481-1486,1525,共7页Systems Engineering and Electronics

基　　金：高等学校博士学科点专项基金(K014010422);"十五"国防预研项目基金(413150501)资助课题

摘　　要：针对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.

关 键 词：统一建模语言 类图 序列图 机械定理 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]