Property transformation under specification change

作     者：Zheng Fu (1) zhengfu@itee.uq.edu.au Graeme Smith (1) 

作者机构：1. School of Information Technology and Electrical Engineering The University of Queensland QLD 4072 Australia 

出 版 物：《Frontiers of Computer Science》 (中国计算机科学前沿（英文版）)

年 卷 期：2011年第5卷第1期

页      面：1-13页

核心收录：

学科分类：12[管理学] 02[经济学] 0202[经济学-应用经济学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 020205[经济学-产业经济学] 08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：formal methods Z refinement temporallogic system property 

摘      要：Formal specifications of software systems need to evolve in many ways during system development. Not only are changes required to refine the specification toward 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 evolution of the specification, but also make precise how 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.