Reverse Engineering from Assembler to Formal Specifications via Program Transformations

TL;DR

This paper presents a case study demonstrating how the FermaT transformation system can convert IBM 370 Assembler code into high-level formal specifications using automated and manual transformations.

Contribution

It introduces a practical application of program transformations for reverse engineering assembler code into formal specifications, showcasing the system's capabilities.

Findings

Successful conversion of assembler code to high-level specifications

Demonstration of automated and manual transformation techniques

Validation of FermaT's effectiveness in program comprehension

Abstract

The FermaT transformation system, based on research carried out over the last sixteen years at Durham University, De Montfort University and Software Migrations Ltd., is an industrial-strength formal transformation engine with many applications in program comprehension and language migration. This paper is a case study which uses automated plus manually-directed transformations and abstractions to convert an IBM 370 Assembler code program into a very high-level abstract specification.