A formal approach for reverse engineering: a case study

As a program evolves, it becomes increasingly difficult to understand and reason about changes in the source code. Eventually, if enough changes are made, reverse engineering and design recovery techniques must be used in order to understand the current behavior of a system. In this context, the effective use of complementary approaches can facilitate program and system understanding by taking advantage of the relative benefits of different approaches. This paper presents an approach to reverse engineering that combines the use of both informal and formal methods and describes a case study project involving the reverse engineering of a mission control system used by the NASA Jet Propulsion Laboratory to command unmanned spacecraft