| 基于Real-Time Object-Z语言的实时系统形式化描述 |
| |
| 引用本文： | 魏艳铭,张广泉. 基于Real-Time Object-Z语言的实时系统形式化描述[J]. 重庆师范大学学报(自然科学版), 2007, 24(4): 41-44 |
| |
| 作者姓名： | 魏艳铭 张广泉 |
| |
| 作者单位： | 1. 重庆师范大学,数学与计算机学院,重庆,400047;河南经贸职业学院,信息管理系,郑州,450053
2. 河南经贸职业学院,信息管理系,郑州,450053 |
| |
| 基金项目： | 重庆市教委科学技术研究项目(No.040803) |
| |
| 摘 要： | 实时系统是一类需要考虑时间约束条件的反应系统,确保实时系统安全性和可靠性是至关重要的。形式化方法是建立在严密数学基础之上的开发方法,采用形式化方法对实时系统进行描述与验证,可以借助严密的数学证明提高实时系统的安全性和可靠性。本文讨论Object-Z的一种实时扩展语言Real-Time Object-Z,它可以对实时系统进行形式化描述;文中以室温控制系统为例,详细说明了Real-Time Object-Z语言在实时系统形式化描述中的应用方法。
|
| 关 键 词： | 实时系统 Object-Z Real-Time Object-Z 实时精化演算 形式化描述 |
| 文章编号： | 1672-6693（2007）04-0041-04 |
| 收稿时间： | 2007-03-26 |
| 修稿时间： | 2007-03-262007-06-27 |
The Formal Specification of Real-Time System Based on Real-Time Object-Z |
| |
| WEI Yan-ming,ZHANG Guang-quan. The Formal Specification of Real-Time System Based on Real-Time Object-Z[J]. Journal of Chongqing Normal University:Natural Science Edition, 2007, 24(4): 41-44 |
| |
| Authors: | WEI Yan-ming ZHANG Guang-quan |
| |
| Affiliation: | 1. College of Mathematics and Computer Science, Chongqing Normal University, Chongqing 400047 ;2. Dept. of Information Management, Henan Economy and Trade Vocational College, Zhengzhou 450053, China |
| |
| Abstract: | |
| |
| Keywords: | real-time system Object-Z Real-Time Object-Z timed refinement calculus formal specification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《重庆师范大学学报(自然科学版)》浏览原始摘要信息 |
|
点击此处可从《重庆师范大学学报(自然科学版)》下载全文 |
