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

赖明志; 尤晋元

您当前的位置：

首页 >

文章列表页 >

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

科研通信 | 更新时间：2025-07-16

- 从UML状态图到PVS规范的自动转换、验证
- Automatic Transform UML Statechart into PVS
- 电子学报 2002年30卷第S1期页码：2122-2125
- 作者机构：
  
  上海交通大学计算机科学与工程系,上海,200030
- 作者简介：
- 基金信息：
  
  国家自然科学基金 (No.69973032)
- DOI：
  中图分类号： TP301
- 纸质出版：2002
- 稿件说明：
移动端阅览
赖明志, 尤晋元. 从UML状态图到PVS规范的自动转换、验证[J]. 电子学报, 2002,30(S1):2122-2125.

LAI Ming-zhi, YOU Jin-yuan. Automatic Transform UML Statechart into PVS[J]. Acta Electronica Sinica, 2002, 30(S1): 2122-2125.
赖明志, 尤晋元. 从UML状态图到PVS规范的自动转换、验证[J]. 电子学报, 2002,30(S1):2122-2125. DOI：

LAI Ming-zhi, YOU Jin-yuan. Automatic Transform UML Statechart into PVS[J]. Acta Electronica Sinica, 2002, 30(S1): 2122-2125. DOI：

摘要

将UML(统一建模语言)图形转换成形式化规范是一种精确化UML语义、扩大形式化软件方法适用范围的有效途径.PVS是一种通用高阶逻辑形式化规范语言

具有很强的描述能力以及丰富的定理证明、模型验证工具支持.本文论证了使用.PVS来对UML进行形式化的优势

并且给出了UML的状态图到PVS规范的转换模型与规则.

Abstract

Formalizing UML diagrams is an effective way to get a precise UML semantics and extend the usage of formal methods.PVS is a higher-order logic based general formal specification langugae with strong expressiveness and foraml analysis tools support. By compring with other formal methods

the advantages of PVS are given in formalizing UML. A hierarchical automata model and algorithms are provided for transforming UML Statechart to PVS specification.

关键词

Keywords

references

浏览量

928

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

暂无数据