基于Real-Time Object-Z语言的实时系统形式化描述  

The Formal Specification of Real-Time System Based on Real-Time Object-Z

作　　者：魏艳铭[1] 张广泉[2] 

机构地区：[1]重庆师范大学数学与计算机学院,重庆400047 [2]河南经贸职业学院信息管理系,郑州450053

出　　处：《重庆师范大学学报（自然科学版）》2007年第4期41-44,53,共5页Journal of Chongqing Normal University:Natural Science

基　　金：重庆市教委科学技术研究项目(No.040803)

摘　　要：实时系统是一类需要考虑时间约束条件的反应系统,确保实时系统安全性和可靠性是至关重要的。形式化方法是建立在严密数学基础之上的开发方法,采用形式化方法对实时系统进行描述与验证,可以借助严密的数学证明提高实时系统的安全性和可靠性。本文讨论Object-Z的一种实时扩展语言Real-Time Object-Z,它可以对实时系统进行形式化描述;文中以室温控制系统为例,详细说明了Real-Time Object-Z语言在实时系统形式化描述中的应用方法。Real-time systems are reactive systems that take into account time constraints. There are many computer control systems belonged to real-time systems, for example, nuclear reactor ,control in aeronautics ,dispatch of railroads and so on. These systems have stronger properties than other systems, such as real-time,concurrent and interactive. Because of their extensive usage in the safety-critical domains, real-time systems lay the most important emphasis on the safety and reliability properties. Based on rigour mathematics, formal methods can use the symbols of mathematics to specification and verify the systems. When formal methods are adopted to specify and verify real-time systems, it is certain to improve safety and reliability of real-time systems under rigour proofs. Formal specification is an important part of research for formal methods, Object-Z is a formal specification language, and it is an extension of Z which is also a formal specification language to facilitate specification in an object-oriented style. It is suitable to specify the complex data structures of systems. Usually a system is comprised of many parts. We use the Object-Z notation to specify the system by specifying a group of individual classes and a systemic class respectively, and we can use the Object-Z notation to specify the object-oriented characteristics conveniently, for example, inheritance and so on. But its utility is limited by its inability to specify continuous variables and real-time constrains. So it is necessary to extend Object-Z for accommodating the requirements of real-time. Real-Time Object-Z discussed in this paper is a real-time extension of Object-Z. It is the integration of Object-Z with timed refinement calculus. The way of the integration does not put forward a suit of new syntax and semantics, but use existing symbols and methods to specify the requirement of systems and import less new symbols to the greatest extend. Primary reason,rules and tools are still usable. Real-time Object-Z can specify not only the

关 键 词：实时系统 OBJECT-Z REAL-TIME OBJECT-Z 实时精化演算 形式化描述 

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