Formal methods to aid the evolution of software.

Simple item page
dc.contributor.authorWard, Martin
dc.contributor.authorBennett, Keith H.
dc.date.accessioned2005-09-05T18:14:34Z
dc.date.available2005-09-05
dc.date.issued2005-09-05
dc.descriptionPaper dated January 6, 1995en
dc.description.abstractThere 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.sponsorshipPartly 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.extent291320 bytes
dc.format.extent226242 bytes
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.identifier.citationWard, 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.doihttps://doi.org/10.1142/S0218194095000034
dc.identifier.otherIR/2005/15
dc.identifier.urihttp://hdl.handle.net/2086/38
dc.language.isoenen
dc.relation.ispartofseriesSTRLen
dc.relation.ispartofseries1995-5en
dc.researchgroupSoftware Technology Research Laboratory (STRL)
dc.subjectAlvey
dc.subjectDTI
dc.subjectSERC
dc.subjectIBM UK
dc.subjectIEATP
dc.titleFormal methods to aid the evolution of software.en
dc.typeArticleen

Files

Original bundle
Now showing 1 - 2 of 2
Thumbnail Image
Name:
evolution-t.pdf
Size:
284.49 KB
Format:
Adobe Portable Document Format
Description:
Main article text
Download
No Thumbnail Available
Name:
evolution-t.ps
Size:
220.94 KB
Format:
Postscript Files
Description:
Main article in postscript
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.78 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

School of Computer Science and Informatics