Zheng Fu (2011). FORMAL PROPERTY PRESERVATION AND TRANSFORMATION IN SOFTWARE EVOLUTION MPhil Thesis, School of Information Technol and Elec Engineering, The University of Queensland.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
s41314344_mphil_finalthesis.pdf Final thesis application/pdf 419.39KB 7
Author Zheng Fu
School, Centre or Institute School of Information Technol and Elec Engineering
Institution The University of Queensland
Publication date 2011-08
Thesis type MPhil Thesis
Supervisor A.Prof. Graeme Smith
Prof. Ian Hayes
Total pages 108
Total black and white pages 108
Language eng
Subjects 08 Information and Computing Sciences
Abstract/Summary Software systems continue to suffer from symptoms of aging due to rapid changes in user requirements and environments. Therefore, software systems need to be constantly maintained and developed. Software evolution, as a key software maintenance theory, provides support for change management at any level of development. One of the challenges in evolution is to verify system correctness after each change, known as re-verification. As software systems tend to be large and complex, reverification can be difficult. It can also be expensive when software development frameworks like formal methods are used. Software development using formal methods is being increasingly applied today, especially for the development of high-integrity, safety-critical and fault-tolerant systems. Although formal methods can contribute to the reliability and robustness of a design through mathematical verification, it not only requires strong logic and mathematical expertise, but often involves manual proofs due to the lack of automated tool support. The difficulty of formal verification becomes even greater when software evolution is taken into account. Unfortunately, formal methods provide very poor support for verifying formal specifications during evolution. This is because, with the current approaches and tools, the re-verification efforts are not proportional to the size of the modifications. For example, even if small changes were to be made to a specification, the entire system would then need to be re-verified. The motivation of this thesis is to improve the current support of software evolution during formal methods in terms of re-verification. The re-use of formal verification during specification evolution is addressed by proposing and presenting property preservation rules. By analyzing the essential meanings of safety and liveness properties, a set of rules is provided to show how properties of the original system can be re-used in an evolved system to reduce verification effort. Moreover, rules are provided to allow the derivation of new properties based on the originals without additional verification. The transformed properties can be used to reflect the consequences of the modifications. The approach is based on the Z and Object-Z specification languages and Linear Temporal Logic properties. The choice of state-based specifications provides an explicit view on making reasonable changes like weakening/strengthening both pre and postconditions of operations. Other modifications like changing initialization and data representation are also discussed to make our approach complete. The overall theory of this thesis is not restricted to Z and Object-Z, and can be applied to other specification languages.
Keyword formal methods, software engineering, software evolution, Z notation, object-Z notation, temporal logic, safety and liveness properties
Additional Notes Final thesis submission

Citation counts: Google Scholar Search Google Scholar
Created: Thu, 05 Jan 2012, 14:15:15 EST by Mr Zheng Fu on behalf of Library - Information Access Service