Publication

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 term model extraction to 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 for model abstraction in 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).