带OCL约束条件的类图到Object-Z规格说明的转换  

Transformation UML Class Diagrams with OCL Constraints into Object-Z Formal Specification

作　　者：缪淮扣[1] 陈怡海[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072

出　　处：《计算机科学》2007年第1期228-235,共8页Computer Science

基　　金：国家自然科学基金(项目编号60373072);国家973项目(批准号2002CB312001);上海市教委第四期重点学科建设基金的资助

摘　　要：如何提高软件的可靠性是目前软件研究领域的一个热点。将形式化方法和主流的软件开发方法相结合是一个可行的方法。本文研究UML语言和Object-Z语言相结合的方法,为主流的软件开发人员所使用的图形化规格说明技术与形式方法提供的精确的分析和验证技术架起了一座桥梁。本文定义如何将带OCL约束条件的类图转换到Object-Z规格说明的方法。这样不仅可以通过支持Object-Z语言的工具来对UML语言描述的系统性质进行验证和确认,而且能够帮助规格说明人员方便地构造Object-Z规格说明。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 Objeet-Z. By this way, we can use the tools supporting Object-Z to vali- date and verify the system properties described by UML class diagrams, and also facilitate the specifier to construct the Object-Z specification.

关 键 词：UML 类图 OCL约束 OBJECT-Z规格说明 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]