Enhancing a behavioral interface specification language with temporal logic features

Date
2009-01-01
Authors
Hussain, Faraz
Major Professor
Advisor
Gary T. Leavens
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Department
Computer Science
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.

Comments
Description
Keywords
Citation
Source