JIVE JML dynamic program verifier
I thought I’d write about my project in my blog so that if someone’s really interested can keep up and learn stuff.
My final year B.Tech project is developing a tool that program that can perform dynamic verification of Java programs. I’ve been doing this for a long time now and know that the blog post is coming rather late but hey better late than never :D.
Program verification is ensuring that a given program does what it’s supposed to do. It sounds easy enough but is probably the most toughest thing to do. It’s kinda related to testing I’d say.
Okay so what’s dynamic about it huh? Why would the act of verification change? Dynamic is actually related to the category of verification algorithms. There are two common approaches in program verification: static and dynamic.
Static verification is mainly based on the structure of the program i.e. no actual execution of the program is performed. It does cover all possible execution paths and thus is a sure shot way of verifying a program but problems such as state explosion(in theorem provers) and program size(in model checking) can prove detrimental to successfully carrying out this approach.
We’re adopting the dynamic approach where data from several runs are obtained and used to perform the verification. This is best suited for large programs but complete coverage of all execution paths isn’t easy. But hey, there’s always a tradeoff in everything we do and that’s why engineers have a profession :P.
Of course the question that comes next is “What data?” This is where JIVE comes in. JIVE stands for Java Interactive Visualization Environment. It’s a tool developed by Computer Science department SUNY, Buffalo that performs some amazing visualization such as class diagram, sequence diagram etc. It also generates logs of events which occur and that is the data that we’ll be using to perform verification.
So now we’ve the data and what are we going to verify against then? JML specifications :)! JML stands for Java Modelling Language-a behavioural specification language for Java programs! It’s an amazingly powerful language that has a huge number of constructs to specify behaviour!
Now comes the ultimate question posed to every developer to find out if it’s just a passing whim and fancy of the developer-why is this idea important? I can simply read code and verify the code myself.
Again that is not easy-think of reading tens of thousands of LoC and performing verification. Not an easy task! Having a tool that can do it and too for almost any code you write is super cool!
Of course there are other advantages that it’s possible to modify and test the specification without having to execute the program. Not just that, there’s no need to add any extra code to assert certain conditions and this allows profiling and verifying the program to be done simultaneously.
And that’s our project in a nutshell-perform dynamic verification of Java programs using the JIVE logs and the JML specifications! Sounds easy to say but really hard to do I’d say. More in the next post!
I’d like to thank our project guide Mr. Jayaraj P, CTO, Amrita Research Lab and Mr. Bharat Jayaraman, Professor, Department of Computer Science and Engineering, The State University of New York, Buffalo and co-ordinator of the Language Research Group at The State University of New York, Buffalo for all the support I’ve received from them in the project. I’d also like to thank Shilpa, my project teammate for having to put with my um idiosyncrasies :P.