| 从UML状态图到PVS规范的自动转换、验证 |
| |
| 引用本文： | 赖明志,尤晋元.从UML状态图到PVS规范的自动转换、验证[J].电子学报,2002,30(Z1):2122-2125. |
| |
| 作者姓名： | 赖明志 尤晋元 |
| |
| 作者单位： | 上海交通大学计算机科学与工程系, 上海, 200030 |
| |
| 基金项目： | 国家自然科学基金，69973032， |
| |
| 摘 要： | 将UML(统一建模语言)图形转换成形式化规范是一种精确化UML语义、扩大形式化软件方法适用范围的有效途径.PVS是一种通用高阶逻辑形式化规范语言,具有很强的描述能力以及丰富的定理证明、模型验证工具支持.本文论证了使用.PVS来对UML进行形式化的优势,并且给出了UML的状态图到PVS规范的转换模型与规则.
|
| 关 键 词： | UML状态图 PVS 层次自动机模型 模型验证 |
| 文章编号： | 0372-2112(2002)12A-2122-04 |
| 收稿时间： | 2002-06-10 |
| 修稿时间： | 2002年6月10日 |
Automatic Transform UML Statechart into PVS |
| |
| LAI Ming-zhi,YOU Jin-yuan.Automatic Transform UML Statechart into PVS[J].Acta Electronica Sinica,2002,30(Z1):2122-2125. |
| |
| Authors: | LAI Ming-zhi YOU Jin-yuan |
| |
| Affiliation: | Depart of Computer Science & Engineering Shanghai Jiao Tong University, Shanghai 200030, China |
| |
| 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: | PVS |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《电子学报》浏览原始摘要信息 |
|
点击此处可从《电子学报》下载全文 |
