开放式体系结构数控系统实时性的建模与分析

• 作者: 叶佩青 张辉 曹宇男 王田苗
• 来源期刊: 机械工程学报
• 学科: 工学
• 关键词: 开放式体系结构数控系统 形式化描述与验证方法 时间转化模型/全时轴实时时态逻辑 实时性 建模
• 年，卷（期）: 2011,（1）
• 所属期刊栏目: 数字化设计与制造
• 页码范围: 108-116
• 分类号: TP391.9
• 字数: 8233字
• 语种: 中文
• DOI: 10.3901/JME.2011.01.108

摘要

给出一个新的用于描述开放式体系结构数控系统(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系统进行建模并对系统的实时特性进行验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	叶佩青	清华大学精密仪器与机械学系	121	1914	24.0	40.0
2	张辉	清华大学精密仪器与机械学系	217	1483	19.0	30.0
3	王田苗	北京航空航天大学机器人所	295	5727	37.0	65.0
4	曹宇男	清华大学精密仪器与机械学系	3	10	1.0	3.0