Abstract Finite‐state models are extensively used for discrete systems and they have also been adopted for the analysis and verification of concurrent systems. Programs that have a repetitive cycle, such as event‐driven servers and controllers, lend themselves to finite‐state modeling. In this article, we use the termmodel extractionto refer to the construction of a finite‐state model from an execution trace of a Java program and a set of key attributes, that is, a subset of the fields of the objects in the program execution. By choosing different sets of attributes, different finite‐state models (or views) of the execution can be obtained. Such models aid program comprehension and they can also be used in debugging a program. We present algorithms for model extraction and also formodel abstractionin order to reduce the size of the extracted models so that they are amenable to visualization. For long executions, we show how to minimize the overhead of execution trace collection through a bytecode instrumentation technique; and, for large models, which are not amenable to visualization, we show how key properties of the extracted model can be checked against declarative specifications. We have implemented our techniques in the context of JIVE, an Eclipse plugin that supports runtime visualization and analysis of Java program executions. We illustrate our techniques through a collection of case studies of varying size and complexity, from classic problems of concurrency control to a medium‐size protocol for authorization (OAuth2.0 protocol) to a large‐scale software that underlies web applications (Apache Tomcat server).

The context of this work is a practical, open-source visualization system, called JIVE, that supports two forms of runtime visualizations of Java programs – object diagrams and sequence diagrams. They capture, respectively, the current execution state and execution history of a Java program. These diagrams are similar to those found in the UML for specifying design–time decisions. In our work, we construct these diagrams at execution time, thereby ensuring continuity of notation from design to execution. In so doing, a few extensions to the UML notation are proposed in order to better represent runtime behavior. As sequence diagrams can become long and unwieldy, we present techniques for their compact representation. A key result in this paper is a novel labeling scheme based upon regular expressions to compactly represent long sequences and an O(r2) algorithm for computing these labels, where r is the length of the input sequence, based upon the concept of ‘tandem repeats’ in a sequence. Horizontal compaction greatly helps minimize the extent of white space in sequence diagrams by the elimination of object lifelines and also by grouping lifelines together. We propose a novel extension to the sequence diagram to deal with out-of-model calls when the lifelines of certain classes of objects are filtered out of the visualization, but method calls may occur between in-model and out-of-model calls. The paper also presents compaction techniques for multi-threaded Java execution with different forms of synchronization. Finally, we present experimental results from compacting the runtime visualizations of a variety of Java programs and execution trace sizes in order to demonstrate the practicality and efficacy of our techniques. Copyright © 2016 John Wiley & Sons, Ltd.