Towards more flexible development of Z specifications

Fu, Z. and Smith, G. (2008). Towards more flexible development of Z specifications. In: J. Davies and X. Li, Theoretical Aspects of Software Engineering 2008 (TASE '08). 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering 2008 (TASE '08), Nanjing, China, (281-288). 17-19 June 2008. doi:10.1109/TASE.2008.20


Author Fu, Z.
Smith, G.
Title of paper Towards more flexible development of Z specifications
Conference name 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering 2008 (TASE '08)
Conference location Nanjing, China
Conference dates 17-19 June 2008
Proceedings title Theoretical Aspects of Software Engineering 2008 (TASE '08)
Journal name Tase 2008: Second Ifip/ieee International Symposium On Theoretical Aspects of Software Engineering, Proceedings
Place of Publication Piscataway, NJ, U.S.A.
Publisher IEEE - Institute of Electrical Electronics Engineers Inc.
Publication Year 2008
Sub-type Fully published paper
DOI 10.1109/TASE.2008.20
Open Access Status
ISBN 978-0-7695-3249-3
Editor J. Davies
X. Li
Start page 281
End page 288
Total pages 8
Language eng
Abstract/Summary Formal specifications of software systems need to evolve in many ways during system development. Not only are changes required to refine the specification towards an implementation, they are also required in response to changes in requirements, or to incorporate different aspects of the system, e.g., fault tolerance or timing, initially ignored in order to simplify reasoning. This paper presents an approach for evolving Z specifications by the step-wise application of a number of simple rules. These rules not only document the specification's evolution, but also make precise how safety properties of the system evolve with the specification. Hence, reasoning about these properties performed on the original specification need not be repeated on the new specification.
Subjects E1
080309 Software Engineering
890299 Computer Software and Services not elsewhere classified
Keyword Z specification
Formal specification
Software system
Q-Index Code E1
Q-Index Status Confirmed Code

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 1 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 2 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Sat, 28 Mar 2009, 01:57:32 EST by Donna Clark on behalf of School of Information Technol and Elec Engineering