Programs
- Ph. D. in Mechanical Engineering -
- B.Tech. in Artificial Intelligence (AI) and Data Science (Medical Engineering) - Undergraduate
Publication Type : Conference Proceedings
Publisher : 2015 Eighth International Conference on Contemporary Computing (IC3), IEEE
Source : Proceedings of Eighth International Conference on Contemporary Computing (IC3), IEEE, Noida, India, p.548-554 (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
Campus : Amritapuri
School : Department of Computer Science and Engineering, School of Engineering
Department : Computer Science
Verified : No
Year : 2015
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