Degree Type

Thesis

Date of Award

2009

Degree Name

Master of Science

Department

Computer Science

First Advisor

Gary T. 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 program's functional behavior. However, for certain applications it is more natural and intuitive to be able to express a system's temporal properties.

This thesis enhances the capabilities of the Java Modeling Language (JML), a behavioral interface specification language, by incorporating 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 program's temporal specifications.

Copyright Owner

Faraz Hussain

Language

en

Date Available

2012-04-28

File Format

application/pdf

File Size

68 pages

Share

COinS