Enhancing a behavioral interface specification language with temporal logic features
by Hussain, Faraz, M.S., IOWA STATE UNIVERSITY, 2009, 68 pages; 1464215

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.

 
AdviserGary T. Leavens
SchoolIOWA STATE UNIVERSITY
SourceMAI/ 47-05, p. , Jul 2009
Source TypeThesis
SubjectsComputer science
Publication Number1464215
Adobe PDF Access the complete dissertation:
 

» Find an electronic copy at your library.
  Use the link below to access a full citation record of this graduate work:
  http://gateway.proquest.com/openurl%3furl_ver=Z39.88-2004%26res_dat=xri:pqdiss%26rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation%26rft_dat=xri:pqdiss:1464215
  If your library subscribes to the ProQuest Dissertations & Theses (PQDT) database, you may be entitled to a free electronic version of this graduate work. If not, you will have the option to purchase one, and access a 24 page preview for free (if available).

About ProQuest Dissertations & Theses
With over 2.3 million records, the ProQuest Dissertations & Theses (PQDT) database is the most comprehensive collection of dissertations and theses in the world. It is the database of record for graduate research.

The database includes citations of graduate works ranging from the first U.S. dissertation, accepted in 1861, to those accepted as recently as last semester. Of the 2.3 million graduate works included in the database, ProQuest offers more than 1.9 million in full text formats. Of those, over 860,000 are available in PDF format. More than 60,000 dissertations and theses are added to the database each year.

If you have questions, please feel free to visit the ProQuest Web site - http://www.proquest.com - or call ProQuest Hotline Customer Support at 1-800-521-3042.