Modeling and analysis of real-time properties of open architecture computerized numerical control systems

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.