Please use this identifier to cite or link to this item: http://hdl.handle.net/10397/26956
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
Dependability
Reliability
Safety
TTM/ATRTTL
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.
URI: http://hdl.handle.net/10397/26956
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

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

Page view(s)

30
Last Week
0
Last month
Checked on Jun 25, 2017

Google ScholarTM

Check

Altmetric



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