A formal specification and verification framework for designing and verifying reliable and dependable software for computerized numerical control (CNC) systems

Yunan Cao, Zili Shao, Meng Wang, Chun Jason Xue, Youdong Chen, Hongxing Wei, Tianmiao Wang

Research output: Chapter in book / Conference proceedingConference article published in proceeding or bookAcademic researchpeer-review

1 Citation (Scopus)


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 logical 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.
Original languageEnglish
Title of host publicationProceedings - The 28th International Conference on Distributed Computing Systems, ICDCS 2008
Number of pages8
Publication statusPublished - 22 Sep 2008
Event28th International Conference on Distributed Computing Systems, ICDCS 2008 - Beijing, China
Duration: 17 Jul 200820 Jul 2008


Conference28th International Conference on Distributed Computing Systems, ICDCS 2008


  • CNC
  • Dependability
  • Distributed computing system
  • Formal specification and verification
  • Reliability
  • Safety

ASJC Scopus subject areas

  • Hardware and Architecture
  • Software

Cite this