| 开放式体系结构数控系统实时性的建模与分析 |
| |
| 引用本文： | 曹宇男,张辉,叶佩青,王田苗.开放式体系结构数控系统实时性的建模与分析[J].机械工程学报,2011,47(1). |
| |
| 作者姓名： | 曹宇男 张辉 叶佩青 王田苗 |
| |
| 作者单位： | 1. 清华大学精密仪器与机械学系,北京,100084
2. 北京航空航天大学机器人所,北京,100191 |
| |
| 基金项目： | 国家数控重大专项(2009ZX04009-012); 国家摩擦学重点实验室(SKLT09B08)资助项目 |
| |
| 摘 要： | 给出一个新的用于描述开放式体系结构数控系统(Open architecture computerized numerical control system,OAC)的建模方法——时间转化模型/全时轴实时时态逻辑(Timed transition model/all-time real-time temporal logic,TTM/ATRTTL)。TTM/ATRTTL提供一整套方法用于对OAC系统的硬实时性和反馈特性进行建模并使用该形式化方法在系统层对OAC系统进行建模。分别给出开环OAC,系统级逻辑控制器以及任务间通信和同步机制的TTM模型,并最终给出具有调度机制的闭环OAC系统TTM模型。该模型为系统验证体系结构的基础。最后,给出系统验证体系结构并用模型验证工具STeP和CAD工具SF2STeP实现之。在系统验证过程中,首先解决STeP中遇到的若干模型验证问题,这些问题包括重写规则,验证规则,状态爆炸问题,以及时间约束限制问题。通过模型验证试验解决OAC系统运行过程中出现的死锁以及系统各模块执行时间约束检验问题。试验结果表明该方法可以有效地对OAC系统进行建模并对系统的实时特性进行验证。
|
| 关 键 词： | 开放式体系结构数控系统 形式化描述与验证方法 时间转化模型/全时轴实时时态逻辑 实时性 建模 |
Modeling and Analysis of Real-time Properties of Open Architecture Computerized Numerical Control Systems |
| |
| CAo Yunan,ZHANG Hui,YE Peiqing,WANG Tianmiao.Modeling and Analysis of Real-time Properties of Open Architecture Computerized Numerical Control Systems[J].Chinese Journal of Mechanical Engineering,2011,47(1). |
| |
| Authors: | CAo Yunan ZHANG Hui YE Peiqing WANG Tianmiao |
| |
| Affiliation: | CAO Yunan1 ZHANG Hui1 YE Peiqing1 WANG Tianmiao2(1.Department of Precision Instruments and Mechanology,Tsinghua University,Beijing 100084,2.Robot Research Institute,Beihang University,Beijing 100191) |
| |
| Abstract: | A novel modeling method called timed transition model/all-time real-time temporal logic(TTM/ATRTTL) for specifying open architecture CNC(OAC) systems is proposed.TTM/ATRTTL provides full support for specifying hard real-time property and feed-back characteristics needed for modeling OAC systems.The formal method is used to model OAC systems from different aspects by specifying the TTM structure of an open-loop OAC,a system-level logic controller,and task communication and synchronization,and obtain the clos... |
| |
| Keywords: | Open architecture computerized numerical control system Formal specification and verification Timed transition model/all-time real-time temporal logic Real-time property Modeling |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
