Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front Comput Sci Chin    2011, Vol. 5 Issue (1) : 1-13    https://doi.org/10.1007/s11704-010-0112-5
RESEARCH ARTICLE
Property transformation under specification change
Zheng FU(), Graeme SMITH
School of Information Technology and Electrical Engineering, The University of Queensland, QLD 4072, Australia
 Download: PDF(230 KB)   HTML
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
Abstract

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.

Keywords formal methods      Z      refinement      temporal logic      system property     
Corresponding Author(s): FU Zheng,Email:zhengfu@itee.uq.edu.au   
Issue Date: 05 March 2011
 Cite this article:   
Zheng FU,Graeme SMITH. Property transformation under specification change[J]. Front Comput Sci Chin, 2011, 5(1): 1-13.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-010-0112-5
https://academic.hep.com.cn/fcs/EN/Y2011/V5/I1/1
Fig.1  
Fig.1  
Fig.2  
Fig.2  
Fig.3  
Fig.3  
Fig.4  Sample paths
Fig.4  Sample paths
Fig.5  Sample paths()
Fig.5  Sample paths()
Fig.6  
Fig.6  
Fig.7  
Fig.7  
Fig.8  
Fig.8  
Fig.9  
Fig.9  
Fig.10  
Fig.10  
Fig.11  
Fig.11  
Fig.12  
Fig.12  
Fig.13  
Fig.13  
Fig.14  
Fig.14  
Fig.15  
Fig.15  
Fig.16  
Fig.16  
1 Woodcock J C P, Davies J. Using Z: Specification, Refinement, and Proof. New Jersey: Prentice Hall, 1996
2 Morgan C C. Programming From Specifications. New Jersey: Prentice Hall, 1990
3 de Roever W P, Engelhardt K. Data Refinement: Model-Oriented Proof Methods and Their Comparison. New York: Cambridge University Press, 1998
doi: 10.1017/CBO9780511663079
4 Swartout W, Balzer R. On the inevitable intertwining of specification and implementation. Communications of the ACM , 1982, 25(7): 438-440
doi: 10.1145/358557.358572
5 van Schouwen A J, Parnas D, Madey J. Documentation of requirements for computer systems. In: Proceedings of 1st IEEE Symposium on Requirements Engineering . 1993, 198-207
6 Hayes I J, Sanders J W. Specification by interface separation. Formal Aspects of Computing , 1995, 7(4): 430-439
doi: 10.1007/BF01211217
7 Guerra S. Defaults in the specification of reactive systems. Dissertation for the Doctoral Degree . London: University College London, 1999
8 Bredereke J. Families of formal requirements in telephone switching. In: Calder M, Magill E H, eds. Feature Interactions in Telecommunications and Software Systems . IOS Press, 2000, 257-273
9 van Lamsweerde A, Darimont R, Massonet P. Goaldirected elaboration of requirements for a meeting scheduler: Problems and lessons learnt. In: Proceedings of 2nd IEEE Symposium on Requirements Engineering . 1995, 194-203
doi: 10.1109/ISRE.1995.512561
10 Liu S. Evolution: A more practical approach than refinement for software development. In: Proceedings of 1997 IEEE International Conference on Engineering of Complex Computer Systems . 1997, 142-151
11 Smith G. Stepwise development from ideal specifications. In: Proceedings of 23rd Australasian Computer Science Conference . 2000, 227-233
12 Banach R, Poppleton M, Jeske C, Stepney S. Engineering and theoretical underpinnings of retrenchment. Science of Computer Programming , 2007, 67(2-3): 301-329
doi: 10.1016/j.scico.2007.04.002
13 Emerson E A. Temporal and Modal Logic. Handbook of Theoretical Computer Science (Vol. B): Formal Models and Semantics . Cambridge: MIT Press, 1990, 995-1072
14 Smith G, Winter K. Proving temporal properties of Z specifications using abstraction. In: Proceedings of 3rd International Conference of Z and B Users . 2003, 260-270
15 Smith G, Wildman L. Model checking Z specifications using SAL. In: Proceedings of 4th International Conference of Z and B Users . 2005, 85-103
16 Derrick J, Boiten E. Refinement in Z and Object-Z: Foundations and Advanced Applications. London: Springer-Verlag, 2001
17 Fu Z, Smith G. Towards more flexible development of Z specifications. In: Proceedings of 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering . 2008, 281-288
doi: 10.1109/TASE.2008.20
18 Peterson G L. Myths about the mutual exclusion problem. Information Processing Letters , 1981, 12(3): 115-116
doi: 10.1016/0020-0190(81)90106-X
19 Smith G. The Object-Z Specification Language. Hingham: Kluwer Academic Publishers, 2000
20 Derrick J, Smith G. Linear temporal logic and Z refinement. In: Proceedings of 10th International Conference on Algebraic Methodology and Software Technology . 2004, 117-131
doi: 10.1007/978-3-540-27815-3_13
21 McComb T, Smith G. A minimal set of refactoring rules for Object-Z. In: Proceedings of 10th IFIP WG 6.1 international conference on Formal Methods for Open Object-Based Distributed Systems . 2008, 170-184
[1] Huichao DUAN, Huiqi HU, Weining QIAN, Aoying ZHOU. Incremental join view maintenance on distributed log-structured storage[J]. Front. Comput. Sci., 2021, 15(4): 154607-.
[2] Houda AKREMI, Sami ZGHAL. DOF: a generic approach of domain ontology fuzzification[J]. Front. Comput. Sci., 2021, 15(3): 153322-.
[3] Cungen CAO, Lanxi HU, Yuefei SUI. Monotonic and nonmonotonic gentzen deduction systems for L3-valued propositional logic[J]. Front. Comput. Sci., 2021, 15(3): 153401-.
[4] Hongbo ZHANG, Xin GAO, Jixiang DU, Qing LEI, Lijie YANG. Tile selection method based on error minimization for photomosaic image creation[J]. Front. Comput. Sci., 2021, 15(3): 153702-.
[5] Abhishek MAJUMDAR, Arpita BISWAS, Atanu MAJUMDER, Sandeep Kumar SOOD, Krishna Lal BAISHNAB. A novel DNA-inspired encryption strategy for concealing cloud storage[J]. Front. Comput. Sci., 2021, 15(3): 153807-.
[6] Wei ZHENG, Ying WU, Xiaoxue WU, Chen FENG, Yulei SUI, Xiapu LUO, Yajin ZHOU. A survey of Intel SGX and its applications[J]. Front. Comput. Sci., 2021, 15(3): 153808-.
[7] Deheng YANG, Yuhua QI, Xiaoguang MAO, Yan LEI. Evaluating the usage of fault localization in automated program repair: an empirical study[J]. Front. Comput. Sci., 2021, 15(1): 151202-.
[8] Yunyun WANG, Jiao HAN, Yating SHEN, Hui XUE. Pointwise manifold regularization for semi-supervised learning[J]. Front. Comput. Sci., 2021, 15(1): 151303-.
[9] Hanze DONG, Zhenfeng SUN, Yanwei FU, Shi ZHONG, Zhengjun ZHANG, Yu-Gang JIANG. Extreme vocabulary learning[J]. Front. Comput. Sci., 2020, 14(6): 146315-.
[10] Yihui LIANG, Han HUANG, Zhaoquan CAI. PSO-ACSC: a large-scale evolutionary algorithm for image matting[J]. Front. Comput. Sci., 2020, 14(6): 146321-.
[11] Fan LIU, Xiaomin JI, Gang HU, Jing GAO. A computer aided design method for car form and its application based on shape parameters[J]. Front. Comput. Sci., 2020, 14(6): 146703-.
[12] Neng HOU, Fazhi HE, Yi ZHOU, Yilin CHEN. An efficient GPU-based parallel tabu search algorithm for hardware/software co-design[J]. Front. Comput. Sci., 2020, 14(5): 145316-.
[13] Jintao GAO, Wenjie LIU, Zhanhuai LI. An adaptive strategy for statistics collecting in distributed database[J]. Front. Comput. Sci., 2020, 14(5): 145610-.
[14] Xuejun WANG, Feilong CAO, Wenjian WANG. Adaptive sparse and dense hybrid representation with nonconvex optimization[J]. Front. Comput. Sci., 2020, 14(4): 144306-.
[15] Tao LIAN, Lin DU, Mingfu ZHAO, Chaoran CUI, Zhumin CHEN, Jun MA. Evaluating and improving the interpretability of item embeddings using item-tag relevance information[J]. Front. Comput. Sci., 2020, 14(3): 143603-.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed