A Novel Modeling Method for Analysis Real-Time Properties of Open Architecture CNC (OAC) Systems

摘要：

In this paper,we propose a novel modelling method called TTM/ATRTTL (Extended Timed Transition Models/All-Time Real-Time Temporal Logics) for specifying OAC systems.TTM/ATRTTL provides full support for specifying hard real-time and feed-back that are needed for modelling OAC systems.We apply our formal method 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 final closedloop OAC TTM with scheduling mechanism that is the foundation of our verification framework.Finally,we propose a verification framework and implement it with STeP and SF2STeP.In the verification,we first solve two problems including rewrite rule and state explosion problem when using STeP for verification,and then conduct experiments for verifying an OAC system for dead-lock.The results show that our method can effectively model and verify OAC systems.

关键词： OAC formal specification and verification TTM/ATRTTL STeP

作者: Yunan Cao Youdong Chen Tianmiao Wang Zili Shao

作者单位: The Robot Research Institute,Beihang University,Beijing 100083,China The Robot Research Institute,Beihang University,Beijing 100083,China, Department of Computing The Hong Kong Polytechnic University,Hung Hom,Kowloon,Hong Kong

会议类型: 国际会议

会议名称: International Conference on Modelling,Identification and Control(模拟、鉴定、控制国际会议)

会议地点: 上海

会议语种:英文

在线出版日期: 2008-06-29（万方平台首次上网日期，不代表论文的发表时间）