Formal methods to aid the evolution of software.

De Montfort University Open Research Archive

Show simple item record Ward, Martin Bennett, Keith H. 2005-09-05T18:14:34Z 2005-09-05 2005-09-05
dc.identifier.citation Ward, M. and Bennett, K.H. (1995) Formal methods to aid the evolution of software. International Journal of Software Engineering and Knowledge Engineering, 5 (1), pp. 25-47.
dc.identifier.other IR/2005/15
dc.description Paper dated January 6, 1995 en
dc.description.abstract There is a vast collection of operational software systems which are vitally important to their users, yet are becoming increasingly difficult to maintain, enhance and keep up to date with rapidly changing requirements. For many these so called legacy systems the option of throwing the system away and re-writing it from scratch is not economically viable. Methods are therefore urgently required which enable these systems to evolve in a controlled manner. The approach described in this paper uses formal proven program transformations, which preserve or refine the semantics of a program while changing its form. These transformations are applied to restructure and simplify the legacy systems and to extract higher-level representations. By using an appropriate sequence of transformation, the extracted representation is guaranteed to be equivalent to the code. The method is based on a formal wide spectrum language, called WSL, with accompanying formal method. Over the last ten years we have developed a large catalogue of proven transformations, together with mechanically verifiable applicability conditions. These have been applied to many software development, reverse engineering and maintenance problems. In this paper, we focus on the results of using this approach in reverse engineering of medium scale, industrial software, written mostly in languages such as assembler and JOVIAL. Results from both benchmark algorithms and heavily modified, geriatric software are summarised. We conclude that formal methods have an important practical role in software evolution. en
dc.description.sponsorship Partly funded bu Alvey project SE-088, partly through a DTI/SERC and IBM UK Ltd. funded IEATP grant "From assembler to Z using formal transformations" and partly by SERC (Science and Engineering Research Council) project "A proof theory for program refinement and equivalence: extensions". en
dc.format.extent 291320 bytes
dc.format.extent 226242 bytes
dc.format.mimetype application/pdf
dc.format.mimetype application/postscript
dc.language.iso en en
dc.relation.ispartofseries STRL en
dc.relation.ispartofseries 1995-5 en
dc.subject Alvey
dc.subject DTI
dc.subject SERC
dc.subject IBM UK
dc.subject IEATP
dc.title Formal methods to aid the evolution of software. en
dc.type Article en
dc.researchgroup Software Technology Research Laboratory (STRL)

Files in this item

This item appears in the following Collection(s)

Show simple item record