Show simple item record

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.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.otherIR/2005/15
dc.identifier.urihttp://hdl.handle.net/2086/38
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.language.isoenen
dc.relation.ispartofseriesSTRLen
dc.relation.ispartofseries1995-5en
dc.subjectAlvey
dc.subjectDTI
dc.subjectSERC
dc.subjectIBM UK
dc.subjectIEATP
dc.titleFormal methods to aid the evolution of software.en
dc.typeArticleen
dc.identifier.doihttps://doi.org/10.1142/S0218194095000034
dc.researchgroupSoftware Technology Research Laboratory (STRL)


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record