TY - GEN
T1 - Consistency of Java run-time behavior with design-time specifications
AU - Jayaraman, Swaminathan
AU - Hari, Dinoop
AU - Jayaraman, Bharat
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2015/12/3
Y1 - 2015/12/3
N2 - 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.
AB - 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.
KW - Design-time specifications
KW - Finite-state machines
KW - Model checking
KW - Run-time consistency
KW - Temporal properties
KW - Uml
KW - Visualization
UR - https://www.scopus.com/pages/publications/84969262754
U2 - 10.1109/IC3.2015.7346742
DO - 10.1109/IC3.2015.7346742
M3 - Conference contribution
AN - SCOPUS:84969262754
T3 - 2015 8th International Conference on Contemporary Computing, IC3 2015
SP - 548
EP - 554
BT - 2015 8th International Conference on Contemporary Computing, IC3 2015
A2 - Amudha, J.
A2 - Gupta, Deepa
A2 - Zola, Jaric
A2 - Nanjangud, Narendra
A2 - Pathak, Animesh
A2 - Prasad, Sushil K.
A2 - Ramesh, Tirumale
A2 - Parashar, Manish
A2 - Kothapalli, Kishore
A2 - Bangalore, Purushotham
A2 - Chaudhary, Sanjay
A2 - Dinesha, K. V.
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 8th International Conference on Contemporary Computing, IC3 2015
Y2 - 20 August 2015 through 22 August 2015
ER -