Enhancing a behavioral interface specification language with temporal logic features

Thumbnail Image
Date
2009-01-01
Authors
Hussain, Faraz
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Research Projects
Organizational Units
Organizational Unit
Journal Issue
Is Version Of
Versions
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

Copyright © Faraz Hussain, 2009. All rights reserved.

Description
Keywords
Citation
DOI
Source
Subject Categories
Copyright
Collections