Publication Type:

Conference Paper

Source:

2015 Eighth International Conference on Contemporary Computing (IC3), IEEE, Noida, India (2015)

URL:

https://ieeexplore.ieee.org/abstract/document/7346742

Keywords:

computational modeling, data visualisation, design-time diagram, design-time specifications, Dynamic analysis, Eclipse, Execution trace, finite-state machines, Formal Specification, Formal verification, Java, Java Interactive Visualization Environment, Java program executions, Java programs, Java run-time behavior, JIVE, Kripke structures, Model checking, open-source plugin, program verification, repetitive behaviour, run-time behavior verification, run-time behaviour, run-time consistency, run-time state diagram, Runtime, Software, system monitoring, temporal properties, UML, UML-like finite-state diagrams, Unified modeling language, Visualization, visualization tool

Abstract:

We present a novel framework for formal verification of run-time behaviour of Java programs. We focus on the class of programs with a repetitive behaviour, such as servers and interactive programs, including programs exhibiting concurrency and non-determinism. The design-time specifications for such programs can be specified as UML-like finite-state diagrams, or Kripke structures, in the terminology of model checking. In order to verify the run-time behavior of a Java program, we extract a state diagram from the execution trace of the Java program and check whether the run-time state diagram is consistent with the design-time diagram. We have implemented this framework as an extension of JIVE (Java Interactive Visualization Environment), a state-of-the-art dynamic analysis and visualization tool which constructs object, sequence, and state diagrams for Java program executions. JIVE is available as an open-source plugin for Eclipse and makes available the execution trace for facilitating analyses of program executions. We have tested our extension on a number of programs, and our experiments show that our methodology is effective in helping close the gap between the design and implementation of Java programs.

Cite this Research Publication

Swaminathan J., Hari, D., and Jayaraman, B., “Consistency of Java run-time behavior with design-time specifications”, in 2015 Eighth International Conference on Contemporary Computing (IC3), Noida, India, 2015.