Home // ICONS 2014, The Ninth International Conference on Systems // View article

Formal Methods for Comparing Behavior of Procedures in Different Languages

Authors:
David Musliner
Michael Boldt
Michael Pelican
Daniel Geschwender

Keywords: procedure equivalence, symbolic execution

Abstract:
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.

Pages: 160 to 165

Copyright: Copyright (c) IARIA, 2014

Publication date: February 23, 2014

Published in: conference

ISSN: 2308-4243

ISBN: 978-1-61208-319-3

Location: Nice, France

Dates: from February 23, 2014 to February 27, 2014