Date of Graduation

1999

Document Type

Thesis

Degree Type

MS

College

Statler College of Engineering and Mineral Resources

Committee Chair

John R. Callahan

Committee Member

James D. Mooney

Abstract

Model Checking has been successfully used for validating the requirements of concurrent systems, but validating requirements does not guarantee a sound implementation. We combine the power of model checking with source code assertions to verify concurrent systems. Assertions have been used for detecting software faults during debugging and for run-time checking in production releases of software. We developed the Model-based Assertion Generator and Extraction Tool (MAGET) to extract a PROMELA state model from an assertion-annotated Java program. The extracted model is then validated against properties specified in linear temporal logic (LTL) and the results of the validation process are used to add or modify assertions in the Java program. This approach serves multiple purposes of verifying the implementation and provides guidance in placing assertions in the source code. We illustrate our approach on a Java simulation of Shuttle Liquid Hydrogen Tanking Subsystem and discuss the results.

Download

Share

COinS