Formal Methods for Comparing Behavior of Procedures in Different Languages

We are developing software tools to compare the behavior of two executable procedures, written in the same or different languages. These tools are useful in situations such as verifying that an automated procedure does the same thing as its manual backup, ensuring that a change to a procedure impacts only the intended behavior, and verifying that a procedure converted to a new language maintains its behavior. Our newest tool translates each procedure into a common language, links the initial conditions of the procedures together, and uses symbolic execution to explore the behavior of every execution path, comparing the behavior of the two procedures on each path. In this paper, we describe our approach in detail and present a case study of applying our tool to NASA procedures that had previously been automatically translated from the Procedure Representation Language (PRL) to the Timeliner scripting language. Our tool easily scaled to these real-world procedures, and identified several bugs in the prototype translator.