Formal framework for designing and verifying reliable software for computerized numerical control (CNC) systems

As a distributed computing system, a CNC system needs to be operated reliably, dependably and safely. How to design reliable and dependable software and perform effective verification for CNC systems becomes an important research problem. A new modeling method called TTM/ATRTTL (Timed Transition Models/All-Time Real-Time Temporal Logics) for specifying CNC systems was proposed. TTM/ATRTTL provided full support for specifying hard real-time and feedback that are needed for modeling CNC systems. A verification framework with verification rules and theorems was proposed and it was implemented with STeP and SF2STeP. The proposed verification framework could check reliability, dependability and safety of systems specified by the TTM/ATRTTL method. The modeling and verification techniques were applied on an open architecture CNC (OAC) system and comprehensive studies were conducted on modeling and verifying a logical controller that is the key part of OAC. The results show that the method can effectively model and verify CNC systems and generate CNC software that can satisfy system requirements in reliability, dependability and safety.