M.S. Thesis Defense - Faraz Hussain

Date: 07 Apr, 2009
Time: 9:30 AM
Location: 223 Atanasoff Hall
Topic: Enhancing a behavioral interface specification language with temporal logic features
Major Professor(s): Gary Leavens


Abstract:

Specification languages help programmers write correct programs and also aid efforts for dynamically checking a software implementation with respect to its desired specifications. Most mainstream specification languages primarily deal with a programs functional behavior. However, for certain applications it is more natural and intuitive to be able to express a system temporal properties.

This thesis enhances the capabilities of the Java Modeling Languag (JML), a behavioral interface specification language, by incorporation temporal logic constructs. The temporal specification grammar used is a modification of the JML temporal extension proposed by K. Trentelman and M. Huisman in their paper Extending JML Specifications with Temporal Logic.

I have modified jmlc, the runtime assertion checker for the Java Modeling Language, so that it also generates runtime assertion checking code to dynamically check a programs temporal specifications.