Dr Martin Ward

Job: Reader in Software Engineering

Faculty: Technology

School/department: School of Computer Science and Informatics

Research group(s): Cyber Technology Institute (CTI) (Software Technology Research Laboratory (STRL))

Address: De Montfort University, The Gateway, Leicester, LE1 9BH, United Kingdom

T: +44 (0)116 207 8480

E: mward@dmu.ac.uk

W: www.tech.dmu.ac.uk/~mward/

 

Personal profile

For the last 20 years or so I have been working on the theory and application of Program Transformations. I have developed a Wide Spectrum Language, called WSL, which is uniquely suitable for program analysis and transformation. In parallel with the language design has been the development of a transformation theory and proof methods, together with methods for program development and inverse engineering. The FermaT Transformation Engine is one result of this research and is now available for downloading under the GNU GPL. A graphical front end for FermaT, the FermaT Maintenance Environment is also available for downloading. A tutorial is available.

A program transformation is an operation which modifies a program into a different form which has the same external behaviour. Both programs and specifications can be written in the same language (namely WSL), this means that transformations can be used to demonstrate that a given program is a correct implementation of a given specification, and to transform a low-level, hard-to-understand assembler language program into a more comprehensible high-level language program, or even to an abstract specification.

Inverse Engineering is the process of extracting high-level abstract specifications from source code using program transformations. It forms the basis for a formal method for reverse engineering from source code to specifications.

At Software Migrations I am working on the FermaT project: an industrial strength program transformation system targeted at reverse engineering, program comprehension and migration between programming languages. The system is currently being used in several migration projects to translate IBM 370 and Intel x86 Assembler modules into equivalent readable and maintainable C and COBOL programs.

Research group affiliations

Software Technology Research Laboratory (STRL)

Publications and outputs 

  • The Formal Semantics of Program Slicing for Non-Terminating Computations
    The Formal Semantics of Program Slicing for Non-Terminating Computations 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.
  • Formality, Agility, Security and Evolution in Software Development
    Formality, Agility, Security and Evolution in Software Development 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.
  • Provably Correct Derivation of Algorithms Using FermaT
    Provably Correct Derivation of Algorithms Using FermaT 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.
  • Assembler Restructuring in FermaT
    Assembler Restructuring in FermaT Ward, Martin
  • Deriving a slicing algorithm via FermaT transformations.
    Deriving a slicing algorithm via FermaT transformations. Ward, Martin; Zedan, Hussein
  • Requirements recovery by Matching Domain ontology and program ontology.
    Requirements recovery by Matching Domain ontology and program ontology. Chen, Feng; Zhou, Hong; Yang, Hongji; Ward, Martin
  • Combining dynamic and static slicing for analysing assembler.
    Combining dynamic and static slicing for analysing assembler. Ward, Martin; Zedan, Hussein
  • Transformational programming and the derivation of algorithms.
    Transformational programming and the derivation of algorithms. Ward, Martin; Zedan, Hussein
  • Towards a multilingual semantic folksonomy.
    Towards a multilingual semantic folksonomy. Magableh, Murad; Cau, A. (Antonio); Zedan, Hussein; Ward, Martin
  • The FermaT maintenance environment tool demonstration.
    The FermaT maintenance environment tool demonstration. Ward, Martin

Click here to view a full listing of Martin Ward's publications and outputs.

Key research outputs

FermaT Transformation Engine

FermaT Maintenance Environment

Research interests/expertise

Program Transformations

Formal Methods

Software Evolution

Qualifications

DPhil

Courses taught

MSc in Software Engineering

Honours and awards

Royal Society Industry Fellowship awarded November 2010

Conference attendance

MetaWSL and Meta-Transformations in the FermaT Transformation System,
Martin Ward and Hussein Zedan, 29th Annual International Computer Software and
Applications Conference, COMPSAC 2005 , Edinburgh, Scotland, July 26-28, 2005

Conditioned Semantic Slicing via Abstraction and Refinement in FermaT
Martin Ward, Hussein Zedan and Tim Hardcastle
9th European Conference on Software Maintenance and Reengineering (CSMR)
Manchester, UK, March 21-23 2005

Legacy Assembler Reengineering and Migration, Martin Ward, Hussein Zedan
and Tim Hardcastle, ICSM2004, The 20th IEEE International Conference
on Software Maintenance , 11th-17th Sept Chicago Illinois, USA.
IEEE Computer Society

Slicing the SCAM Mug: A Case Study in Semantic Slicing, Martin Ward
Third IEEE International Workshop on Source Code Analysis and Manipulation,
27th September 2003, Amsterdam, Netherlands. IEEE Computer Society.

Program Slicing via FermaT Transformations, M. Ward 26th Annual International Computer Software and Applications Conference, COMPSAC 2002 , Oxford, England, 26th-29th August 2002 IEEE Computer Society.

ConSUS: A Scalable Approach to Conditioned Slicing, M. Daoudi, L. Ouarbya, J. Howroyd, S. Danicic, Mark Harman, Chris Fox, M. P. Ward 9th IEEE Working Conference on Reverse Engineering , 2002. October 28--November 1, 2002 Richmond, Virginia, USA IEEE Computer Society

The Formal Transformation Approach to Source Code Analysis and Manipulation, M. Ward, Keynote speech at the First International Workshop on Source Code Analysis and Manipulation, 10th November 2001, Florence, Italy IEEE Computer Society

The FermaT Assembler Re-engineering Workbench, M. Ward International Conference on Software Maintenance 2001, 6th-9th November 2001, Florence, Italy, IEEE Computer Society

Reverse Engineering from Assembler to Formal Specifications via Program Transformations, M. Ward 7th Working Conference on Reverse Engineering,
23-25th November 2000, Brisbane, Queensland, Australia IEEE Computer Society

Assembler to C Migration using the FermaT Transformation System, M. Ward
International Conference on Software Maintenance, 30th Aug--3rd Sept 1999, Oxford, England.

Current research students

First supervisor for:

Alazemi, Fayez Eid
Barnawi, Abdullah Omar
Alharbi, Mafawez
Almarri, Salem
Mansour Habib AL-QATTAN
Rahuma, Awatef Mohamed
Alghanim, Waleed Ibrahim

Second supervisor for:

Allehaibi, Khalid
Almutairi, Abdulgader Zaid
Huang, Jianchu
Wang, Xuan

Externally funded research grants information

Alvey SEE/088: "A Knowledge-Based System for Software Maintenance", 1988--1991. P.I. , (£40,000)

IED, No. 1266 (IBM and DTI): "ReForm: Reverse Engineering through Formal Methods",1991--1994. P.I. and Technical Leader , ($1.1M)

Software Migrations Ltd.: "GREET: Generic Reverse Engineering Tool", 1992--1997. P.I. , (£550,000)

DTI: SMART (Small Firms Merit Award for Research and Technology) "Using Formal Methods to Analyse Real Time Systems", 1992. P.I. (£45,000)

DTI: SMART II (Small Firms Merit Award for Research and Technology) "Using Formal Methods to Analyse Real Time Systems", 1993. P.I. , (£60,000)

EPSRC: : "Extensions to the program transformation theory to cope with parallel programs and real time issues", 1994 --1996. P.I. , (£45,000)

ESPRIT -- No. 8156: "AMES: Methods and tools for the effective support of Application Management", 1993 --1996. Technical Consultant (£224,000)

EPSRC (GR/R56099/01 15-1-382-1514): "Re-Engineering Large Programs With Program Transformations", 2002--2005. P.I. , (£55,000)

Software Migrations Ltd.: "Software Evolution", 2001 -- 2009. Co Investigator , (£350,000)

Royal Society Industry Fellowship : "An Industrial Strength Software Reengineering Approach ", 2009 -- 2013. P.I. , (£96,000)

Professional esteem indicators

I have been invited to participate on the Program Committees for a number of international academic conferences. These include:

The Working conference on Reverse Engineering

The International Workshop on Source Code Analysis and Manipulation

In February 2009 I was invited to Paris to deliver a lecture to the ReTrust European project (a consortium of five academic and industrial partners from France, Italy, Belgium and Russia) describing the current "state of the art" for reverse engineering.

Case studies

"Conditioned Semantic Slicing for Abstraction; Industrial Experiment", Martin Ward, Hussein Zedan, Matthias Ladkau and Stefan Natelberg Software Practice and Experience, Vol 38, Issue 12, pp 1273-1304, October 2008 doi:doi.wiley.com/10.1002/spe.869

“Combining Dynamic and Static Slicing for Analysing Assembler” Martin Ward and Hussein Zedan Science of Computer Programming, Volume 75, Issue 3, March 2010, Pages 134-175, doi:dx.doi.org/10.1016/j.scico.2009.11.001

martin ward

Search Who's Who

 

 
News target area image
News

DMU is a dynamic university, read about what we have been up to in our latest news section.

Events target area image
Events

At DMU there is always something to do or see, check out our events for yourself.

Mission and vision target area image
Mission and vision

Read about our mission and vision and how these create a supportive and exciting learning environment.