This research will explore the development of an integrated software testing framework that enables source code instrumentation, test case extraction, analysis of test traces, symbolic reasoning about test traces and source code, algebraic specification of software behavior including specifications extracted from test traces, and validation of observed behavior against algebraic specifications. The infrastructure will support the collection and aggregation of test traces, the direct derivation state machine descriptions from event traces, the testing and validation of functional specifications with respect to system behavior, and the verification of system consistency with specifications by validating execution traces against the specifications. Extracted test traces and derived specifications will be tied to source code in a way amenable to viewing by engineers. Tests and their captured data will be cataloged to be both auditable and repeatable, enabling unit and system regression testing. Emphasis will be placed on the consideration of asynchronous systems, including state machine derivation and analysis with respect to temporal logic formulas. The infrastructure for developing these capabilities will be a generalized compiler technology that supports the semantic analysis of source code and other structures as well as the capability for implementing mass changes in source code by automatic transformation.
Keywords: SOFTWARE TESTING, SOFTWARE INSTRUMENTATION, TEST CASE GENERATION, STATIC ANALYSIS, DYNAMIC ANALYSIS, DATA ABSTRACTION, FORMAL VERIFICATION, SOFTWARE VALIDATION
