| 带OCL约束条件的类图到object—Z规格说明的转换 |
| |
| 引用本文： | 缪淮扣,陈怡海.带OCL约束条件的类图到object—Z规格说明的转换[J].计算机科学,2007,34(1):228-235. |
| |
| 作者姓名： | 缪淮扣 陈怡海 |
| |
| 作者单位： | 上海大学计算机工程与科学学院,上海,200072 |
| |
| 基金项目： | 国家自然科学基金
,
国家重点基础研究发展计划(973计划)
,
上海市教委资助项目 |
| |
| 摘 要： | 如何提高软件的可靠性是目前软件研究领域的一个热点。将形式化方法和主流的软件开发方法相结合是一个可行的方法。本文研究UML语言和Object-Z语言相结合的方法，为主流的软件开发人员所使用的图形化规格说明技术与形式方法提供的精确的分析和验证技术架起了一座桥梁。本文定义如何将带0CL约束条件的类图转换到Object-Z规格说明的方法。这样不仅可以通过支持Object-Z语言的工具采对UML语言描述的系统性质进行验证和确认，而且能够帮助规格说明人员方便地构造Object-Z规格说明。
|
| 关 键 词： | UML 类图 OCL约束 Object-Z规格说明 |
Transformation UML Class Diagrams with OCL Constraints into Object-Z Formal Specification |
| |
| MIAO Huai-Kou,CHEN Yi-Hai.Transformation UML Class Diagrams with OCL Constraints into Object-Z Formal Specification[J].Computer Science,2007,34(1):228-235. |
| |
| Authors: | MIAO Huai-Kou CHEN Yi-Hai |
| |
| Affiliation: | School of Computer Engineering and Science, Shanghai University, Shanghai 200072 |
| |
| Abstract: | How to improve the software reliability is the hot research topic in the field of software engineering. Integrating formal methods and mainstream software development methods is a viable approach. The integration of UML and Object-Z provides a bridge between graphical specification techniques used by mainstream software engineers, and the precise analysis and verification techniques provided by formal methods. In this paper, we define a translation from UML class diagram with OCL constraints into Object-Z. By this way, we can use the tools supporting Object-Z to validate and verify the system properties described by UML class diagrams, and also facilitate the specifier to construct the Object-Z specification. |
| |
| Keywords: | UML Class diagram OCL constraints Object-Z specification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
