从UML状态图到PVS规范的自动转换、验证

• 作者: 尤晋元 赖明志
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: UML状态图 PVS 层次自动机模型 模型验证
• 年，卷（期）: 2002,（z1）
• 所属期刊栏目: 科研通信
• 页码范围: 2122-2125
• 页数: 4页
• 分类号: TP301
• 字数: 3918字
• 语种: 中文
• DOI: 10.3321/j.issn:0372-2112.2002.z1.051

摘要

将UML(统一建模语言)图形转换成形式化规范是一种精确化UML语义、扩大形式化软件方法适用范围的有效途径.PVS是一种通用高阶逻辑形式化规范语言,具有很强的描述能力以及丰富的定理证明、模型验证工具支持.本文论证了使用PVS来对UML进行形式化的优势,并且给出了UML的状态图到PVS 规范的转换模型与规则.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	尤晋元	上海交通大学计算机科学与工程系	99	1122	18.0	30.0
2	赖明志	上海交通大学计算机科学与工程系	4	69	3.0	4.0