Formal methods to aid the evolution of software.

Date

2005-09-05

Advisors

Journal Title

Journal ISSN

ISSN

Volume Title

Publisher

Type

Article

Peer reviewed

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.

Description

Paper dated January 6, 1995

Keywords

Alvey, DTI, SERC, IBM UK, IEATP

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.

Rights

Research Institute