We investigate the re-engineering of time-critical applications using an integration of refinement and transformational techniques. Our approach is uniform in the sense that we are able to combined both reverse and forward engineering within the same formal model. The approach is based on designing a wide-spectrum language which is equipped with a specification statement and concrete constructs to cope with concurrency and real-time aspects. The language is an extension of Dijkstra's guarded command language with the specification statement taken as a formula expressed in Interval Temporal Logic (ITL). An ITL semantics for our WSL is given together with a set of algebraic laws and refinement rules. Reverse engineering is achieved by applying various algebraic laws to produce a structured code (written in our WSL) from the original one preserving its semantic equivalence. Such a transformation is done semi-automatically using an extension to MA. The resulting code is considered as an intermediate representation which can then be analysed and used as a basis to construct a higher level of abstraction of the original system.Calculating ITL semantics for the intermediate representation serves as a requirement specification of the original code and is subsequently used as the starting point to forward engineer the system by successive applications of the available refinement calculus. The semantics (an ITL formula) is produced automatically with the help of our PVS+ toolkit.