Understanding an unfamiliar program is always a daunting task for any programmer, either experienced or inexperienced. Many studies have shown that even an experienced programmer who is already familiar with the code may still need to rediscover the code frequently during maintenance activities. Compared to that tracing the source code of an unfamiliar program is a totally different process of comprehension. Difficulties in such a process can be compounded if the code has poor or little internal program documentation. In practice, internal program documentation is often neglected or receives much less attention while most documentation techniques are designed to help programmers deal with familiar code, not unfamiliar code. In this paper, a novel internal program documentation method is proposed. In the approach, the multimedia documents, such as slides and voice recording, can be created along with a sequence of debugging break points, where the sequence of break points and its associated multimedia documents form a trace case. We show that trace cases can be very useful in documenting major control flows of a program using examples so that the time needed to construct a program model for understanding can be shortened. To demonstrate the idea, a prototype tool called polyTraceAid has been implemented as a plug-in in Visual Studio.

Regression testing is an indispensable process in software development, which ensures stable features have not been adversely broken by new changes. When GUI plays an important role in an application, a popular choice to automate the tests is applying GUI Capture/Replay tools. Unfortunately, in many applications which render images as output, the correctness of a replay run can no longer be straightforwardly verified. In this paper, we propose a test automation solution, called Intrusive Test Automation, which uses program instrumentation technique to collect the runtime internal information of a program. As a result, the correctness of a test run can be verified by the runtime traces. In addition, when large number of failed test cases are reported by the test automation system, recommending some representative test cases as a start for debugging can be helpful to programmers. This paper proposes a clustering technique based on the information collected from the instrumented code. In principle, fixing bugs in one representative test case can fix its related failed test cases as well. A case study is presented to demonstrate the effectiveness of the approach.

Automated finite-state verification techniques have matured considerably in the past several years, but state-space explosion remains an obstacle to their use. Theoretical lower bounds on complexity imply that all of the techniques that have been developed to avoid or mitigate state-space explosion depend on models that are "well-formed" in some way, and will usually fail for other models. This further implies that, when analysis is applied to models derived from designs or implementations of actual software systems, a model of the system "as built" is unlikely to be suitable for automated analysis. In particular, compositional, hierarchical analysis (where state-space explosion is avoided by simplifying models of subsystems at several levels of abstraction) depend on the modular structure of the model to be analyzed. We describe how as-built finite-state models can be refactored for compositional state-space analysis, applying a series of transformations to produce an equivalent model whose structure exhibits suitable modularity. The process is supported by a parser which can parse a subset of Promela syntax and transform Promela code into refactored state graphs.

Systems composed of many identical processes can sometimes be verified inductively using a network invariant, but systems whose component processes vary in some systematic way are not amenable to direct application of that method. We describe how variations in behavior can be "factored out" into additional processes, thus enabling induction over the number of processes. The process is semi-automatic: The designer must choose from among a set of idiomatic transformations, but each transformation is applied and checked automatically.