Please use this identifier to cite or link to this item:
Title: A formal specification and verification framework for designing and verifying reliable and dependable software for computerized numerical control (CNC) systems
Authors: Cao, Y
Shao, Z 
Wang, M
Xue, C
Chen, Y
Wei, H
Wang, T
Keywords: CNC
Distributed computing system
Formal specification and verification
Issue Date: 2008
Publisher: IEEE
Source: The 28th International Conference on Distributed Computing Systems, 2008 : ICDCS '08, 17-20 June 2008, Beijing, p. 269-276 How to cite?
Abstract: 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 CNCsystems. 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.
ISBN: 978-0-7695-3172-4
978-0-7695-3172-4 (E-ISBN)
ISSN: 1063-6927
DOI: 10.1109/ICDCS.2008.21
Appears in Collections:Conference Paper

View full-text via PolyU eLinks SFX Query
Show full item record

Page view(s)

Last Week
Last month
Citations as of Aug 13, 2018

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.