关键词: 建模, 开放式体系结构数控系统, 时间转化模型/全时轴实时时态逻辑, 实时性, 形式化描述与验证方法

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 closed-loop OAC TTM with scheduling mechanism is given, which is the foundation of the verification framework. Finally, a verification framework is proposed and implemented with STeP and SF2STeP. In the verification, several problems are solved including rewrite rule, verification rule, state explosion problem, and time bound restriction when STeP is used for verification, and then experiments are conducted for verifying an OAC system for dead-lock and system time bound checking. The results show that the method can effectively model and verify OAC systems.

Key words: Formal specification and verification, Modeling, Open architecture computerized numerical control system, Real-time property, Timed transition model/all-time real-time temporal logic