Browsing by Author "Ward, Martin"

Now showing 1 - 20 of 27
  • No Thumbnail Available
    ItemMetadata only
    Assembler Restructuring in FermaT
    (IEEE, 2013) Ward, Martin
  • Thumbnail Image
    ItemOpen Access
    Assembler to C migration using the FermaT transformation system
    (2005-09-05) Ward, Martin
    The FermaT transformation system, based on research carried out over the last twelve years at Durham University and Software Migrations Ltd., is an industrial-strength formal transformation engine with many applications in program comprehension and language migration. This paper describes one application of the system: the migration of IBM 370 Assembler code to equivalent, maintainable C code. We present an example of using the tool to migrate a small, but complex, assembler module to C with no manual intervention required. We briefly discuss a mass migration exercise where 1,925 assembler modules were successfully migrated to C code.
  • No Thumbnail Available
    ItemMetadata only
    Combining dynamic and static slicing for analysing assembler.
    (Elsevier, 2010) Ward, Martin; Zedan, Hussein
  • No Thumbnail Available
    ItemMetadata only
    Conditioned semantic slicing for abstraction; industrial experiment.
    (John Wiley & Sons, 2008-10) Ward, Martin; Zedan, Hussein; Ladkau, Matthias; Natelberg, Stefan
  • No Thumbnail Available
    ItemMetadata only
    Conditioned semantic slicing via abstraction and refinement in FermaT.
    (IEEE, 2005) Ward, Martin; Zedan, Hussein; Hardcastle, T.
  • No Thumbnail Available
    ItemMetadata only
    ConSUS: a light-weight program conditioner
    (Elsevier, 2005-09-01) Ward, Martin; Danicic, S.; Daoudi, M.; Fox, C.
  • Thumbnail Image
    ItemOpen Access
    A definition of abstraction.
    (John Wiley, 2005-07-13) Ward, Martin
    What does it mean to say that one program is "more abstract" than another? What is "abstract" about an abstract data type? What is the difference between a "high-level" program and a "low-level" program? In this paper we attempt to answer these questions by formally defining an abstraction relation between programs which matches our intuitive ideas about abstraction. The relation is based on examining the operational semantics of the programs, expressed as a set of traces (sequences of states) from a given initial state to a possible final state.
  • Thumbnail Image
    ItemOpen Access
    Derivation of data intensive algorithms by formal transformation: the Schorr-Waite graph marking algorithm
    (2005-09-05) Ward, Martin
    In this paper we consider a particular class of algorithms which present certain difficulties to formal verification. These are algorithms which use a single data structure for two or more purposes, which combine program control information with other data structures or which are developed as a combination of a basic idea with an implementation technique. Our approach is based on applying proven semantics-preserving transformation rules in a wide spectrum language. Starting with a set theoretical specification of “reachability” we are able to derive iterative and recursive graph marking algorithms using the “pointer switching” idea of Schorr and Waite. There have been several proofs of correctness of the Schorr-Waite algorithm, and a small number of transformational developments of the algorithm. The great advantage of our approach is that we can derive the algorithm from its specification using only general-purpose transformational rules: without the need for complicated induction arguments. Our approach applies equally well to several more complex algorithms which make use of the pointer switching strategy, including a hybrid algorithm which uses a fixed length stack, switching to the pointer switching strategy when the stack runs out.
  • No Thumbnail Available
    ItemMetadata only
    Deriving a slicing algorithm via FermaT transformations.
    (IEEE, 2011) Ward, Martin; Zedan, Hussein
  • No Thumbnail Available
    ItemMetadata only
  • Thumbnail Image
    ItemOpen Access
    Formal methods for legacy systems.
    (2005-09-05) Ward, Martin; Bennett, Keith H.
    A method is described for obtaining useful information from legacy code. The approach uses formal proven program transformations, which preserve for refine the semantics of a construct while changing its form. The applicability of a transformation in a particular syntactic context is checked before application. By using an appropriate sequence of transformations, the extracted representation is guaranteed to be equivalent to the code. In this paper, we focus on the results of using this approach in the 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. It is concluded that the approach is viable, for self-contained code, and that useful design information may be extracted from legacy systems at economic cost. We conclude that formal methods have an important practical role in the reverse engineering process.
  • Thumbnail Image
    ItemOpen Access
    Formal methods to aid the evolution of software.
    (2005-09-05) Ward, Martin; Bennett, Keith H.
    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.
  • Thumbnail Image
    ItemOpen Access
    The Formal Semantics of Program Slicing for Non-Terminating Computations
    (Wiley, 2016) Ward, Martin
    Since the original development of program slicing in 1979 [.Weiser slices 1979.] there have been many attempts to define a suitable semantics which will precisely define the meaning of a slice. Particular issues include handling termination and non-termination, slicing non-terminating programs and slicing nondeterministic programs. In this paper we review and critique the main attempts to construct a semantics for slicing and present a new operational semantics which correctly handles slicing for non-terminating and nondeterministic programs. We also present a modified denotational semantics which we prove to be equivalent to the operational semantics. This provides programmers with two different methods to prove the correctness of a slice or a slicing algorithm, and means that the program transformation theory and FermaT transformation system, developed over the last 25 years of research, and which has proved so successful in analysing terminating programs, can now be applied to non-terminating interactive programs.
  • Thumbnail Image
    ItemEmbargo
    Formality, Agility, Security and Evolution in Software Development
    (IEEE, 2014-10) Bowen, J. P.; Hinchey, Mike; Janicke, Helge; Ward, Martin; Zedan, Hussein
    Combining formal and agile techniques in software development has the potential to minimize change-related problems.
  • No Thumbnail Available
    ItemMetadata only
    Legacy assembler reengineering and migration.
    (2004-09-01) Ward, Martin; Hardcastle, T.; Zedan, Hussein
  • No Thumbnail Available
    ItemMetadata only
    METAWSL and meta-transformations in the FermaT transformation system.
    (IEEE, 2005) Ward, Martin; Zedan, Hussein
  • No Thumbnail Available
    ItemMetadata only
  • Thumbnail Image
    ItemOpen Access
    Program analysis by formal transformation
    (2005-09-05) Ward, Martin
    This paper treats Knuth and Szwarcfiter’s topological sorting program, presented in their paper “A structured program to generate all topological sorting arrangements” (Knuth and Szwarcfiter 1974), as a case study for the analysis of a program by formal transformations. This algorithm was selected for the case study because it is a particularly challenging program for any reverse engineering method. Besides a complex control flow, the program uses arrays to represent various linked lists and sets, which are manipulated in various “ingenious” ways so as to squeeze the last ounce of performance from the algorithm. Our aim is to manipulate the program, using semantics-preserving operations, to produce an abstract specification. The transformations are carried out in the WSL language, a “wide spectrum language” which includes both low-level program operations and high level specifications, and which has been specifically designed to be easy to transform.
  • No Thumbnail Available
    ItemMetadata only
    Properties of slicing definitions.
    (IEEE, 2009) Ward, Martin
  • Thumbnail Image
    ItemOpen Access
    Provably Correct Derivation of Algorithms Using FermaT
    (Springer, 2014) Ward, Martin; Zedan, Hussein
    The transformational programming method of algorithm derivation starts with a formal specification of the result to be achieved, plus some informal ideas as to what techniques will be used in the implementation. The formal specification is then transformed into an implementation, by means of correctness-preserving refinement and transformation steps, guided by the informal ideas. The transformation process will typically include the following stages: (1) Formal specification (2) Elaboration of the specification, (3) Divide and conquer to handle the general case (4) Recursion introduction, (5) Recursion removal, if an iterative solution is desired, (6) Optimisation, if required. At any stage in the process, sub-specifications can be extracted and transformed separately. The main difference between this approach and the invariant based programming approach (and similar stepwise refinement methods) is that loops can be introduced and manipulated while maintaining program correctness and with no need to derive loop invariants. Another difference is that at every stage in the process we are working with a correct program: there is never any need for a separate "verification" step. These factors help to ensure that the method is capable of scaling up to the development of large and complex software systems. The method is applied to the derivation of a complex linked list algorithm and produces code which is over twice as fast as the code written by Donald Knuth to solve the same problem.