Specification and Test Based Reverse Engineering of Low Level Code System (EDAMarksman)

There is an urgent need in the military to upgrade and re-implement low-level software embedded in operational weapon systems, despite the millions of lines of often undocumented code. EDAptive Computing, Inc. (ECI) presents an innovative solution to the problem of creating specifications from low level code, such as assembly and CMS-2. Our Specification and Test Based Reverse Engineering of Low Level Code System (EDAMarksman) program will apply a combination of formal specification, reverse engineering (compilation), and test generation to provide a specification-based system for testing. Specifically, we propose to utilize an iterative approach to 1) derive specifications from existing code using formal reverse engineering techniques, 2) derive tests from the specifications, 3) apply the tests to the original code and receive feedback, and 4) update the specifications based on test results. Tests produced from specifications will be used to validate the specifications, indicating where tests fail on the actual system, and guide the production of new specifications. The result of this solution will be a specification creation process that will be verified by the actual execution of the system, as guided by the generated specification. We will use a real-life Navy/DoD system as a candidate Phase I demonstration vehicle.