Understanding concurrent programs using program transformations

Reverse engineering of concurrent real-time programs with timing constraints is a particularly challenging research area, because the functional behaviour of a program, and the non-functional timing requirements, are implicit and can be very difficult to discover. The authors present a significant advance in this area, which is achieved by modelling real-time concurrent programs in the wide spectrum language WSL. They show how a sequential program with interrupts can be modelled in WSL, and the method is then extended to model more general concurrent programs. They show how a program modelled in this way may subsequently be `inverse engineered´ by the use of formal program transformations, to discover a specification for the program