« Learning how to run a research lab | Main | Journal on Emergent Algorithms »
September 27, 2005
Application Server and Web Applicaiton Verification
One of my PhD studnets, Tonglaga Bao, and I are embarking on a study of how to reason about application servers (such as JBoss) and web applications built on top of application servers. Rather than build an formal model of an application server, which usually requires abstracting away interesting details, we are going to take a less rigourous but more useful (we hope!) approach. Our approach is to verify the web application using the execution semantics defined by a given application server in a given configuration. We will do this by turning an applicaiton server into a model checker, or something like that. A model checker is a tool that checks if a transition system is a model of a given temporal logic formula. In our case, the transition system is a web application interpreted by an application server, the temporal logic formula describes things like "deadlock free" "no race conditions" "no starvation" etc. The web application is deadlock free (or whatever was specified) if it models, or satisfies, the formula.
I have been reading about application servers and J2EE and will post my learnings as they come. Meanwhile, I was encouraged to find that a Google Search for j2ee returns "do you want to work for google" as the top hit. Good for Tonga!
The insight I had today while reading Teach yourself J2EE in 21 days is that the n-tier architecture and components framework actually supports verification of components. Component verification is something that I studied and loved as an MS student but the work was not as succesful as I'd hoped. So this may be a place to play with those ideas again.
We are actively looking for funding to support this work. If you are interested in participating or contributing to this work, please contact me
Posted by jones at September 27, 2005 03:35 PM
Comments
Post a comment
Thanks for signing in, . Now you can comment. (sign out)
(If you haven't left a comment here before, you may need to be approved by the site owner before your comment will appear. Until then, it won't appear on the entry. Thanks for waiting.)