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

关键词：开放式体系结构数控系统 形式化描述与验证方法 实时性 建模 

单位：清华大学精密仪器与机械学系 北京100084 北京航空航天大学机器人所 北京100191