论文部分内容阅读
针对UML类图和序列图的一致性问题，在充分考虑了类继承关系、关联关系、类方法的可见性以及类方法的前、后置条件等因素对一致性影响的基础上，给出了判定类图和序列图一致性的必要条件和PVS元理论。提出了一种基于定理证明器PVS的一致性检验方法。在检验UML模型一致性时，把一致性检验问题转化为逻辑定理证明问题。实践表明，该方法对于提高UML模型的可信度，减少系统实现阶段的错误起到了一定作用。