基于UML需求建模的一种形式化分析方法及其应用

( ) 第 27 卷第 3 期 沈阳师范大学学报 自然科学版 Vol . 27 No. 3 ( ) 2009 年 7 月 J ou rnal of S heny ang N orm al University N at u ral S cience J ul . 2009 文章编号 : 1673 - 5862 (2009) 03 - 033 1 - 04 基于UML 需求建模的一种形式化 分析方法及其应用 江 　春 (苏州大学 计算机科学与技术学院 , 江苏 苏州 　2 15006) 摘 　　　要 : U ML 是软件开发过程中广泛使用的建模语言 ,但由于缺乏精确的语义 ,难以直接对 其建立的需求模型进行精化和验证 , 因而无法进一步提高软件的正确性和可靠性 ,也不具备实现 软件 自动化的前提条件 。提出了一种基于 U ML 需求建模进行形式化分析的方法 。采用 Obj ectZ 对 U ML 建立的需求模型进行形式化描述 ,采用 Perfect 弥补了 Obj ectZ 在精化与验证方面缺少 自 动化工具支持的不足 ,最后通过一个实例说明了该方法在实际应用中的可行性 。 关 　键 　词 : U ML ; Obj ectZ ; Perfect ; 形式化方法 中图分类号 : TP 3 11 　　　文献标志码 : A U ML [ 1 ] 是一种半形式化的建模语言 ,缺乏精 Obj ectZ 的类结构 。 确的语义 ,用它建立的软件需求模型一方面在用 ClasName [ generic parameter s ] 户需求的语义描述上会存在歧异问题 ,交流时容 Visibilit y list Inherited classes 易产生误解 ,另一方面也难以精化和验证 。针对 Type definitons 这一问题 ,形式化方法[2 ] 可以与之互补 , 它能够 Constand definitions State schema 提供描述手段以精确 、无二义地描述系统 ;提供分 Initial state schema 析手段以严格地证明系统的正确性 ;提供精化手 Operation schemas History invariant 段 以等价地转化形式化描述到高级程序语言 代码 。 图 1 　Obj ectZ 的类结构 为此 , 本 文 探 讨 了一 种 利 用 Obj ectZ 和 Perfect [4 ] 是基于一阶谓词逻辑和集合论的形 Perfect 对基于 U ML 的需求建模进行形式化描述 式化语言 ,支持面向对象的形式化描述 ,能够创