A Formal Specification Framework for Designing and Verifying Reliable and Dependable Software for 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. In this paper, we propose a new modeling method called TTM/ATRTTL (timed transition models/all-time real-time temporal logics) for specifying CNC systems. TTM/ATRTTL provides full supports for specifying hard real time and feedback that are needed for modeling CNC systems. We also propose a verification framework with verification rules and theorems and implement it with STeP and SF2STeP. The proposed verification framework can check reliability, dependability, and safety of systems specified by our TTM/ATRTTL method. We apply our modeling and verification techniques on an open architecture CNC (OAC) system and conduct comprehensive studies on modeling and verifying a system controller that is the key part of OAC. The results show that our method can effectively model and verify CNC systems and generate CNC software that can satisfy system requirements in reliability, dependability, and safety.