Graduate Topics for CS 378/395T

S. Lakshminarasimhan

I have chosen to base my project on the analysis of the Java verification tool - Java PathFinder. The project will constitute the following parts:

A survey of the Java Pathfinder and Pathexplorer tools.
Architecture of Java Pathfinder
How JPF translates Java to Promela (language used by SPIN), A survey of SPIN model checker and how SPIN and JPF work together.
A case study of the application of JPF to find errors in NASA's remote agent space craft controller
A demo of JPF

[link]

Cathy (Yang) Liu

[link]

Carissa Marie Miller

[link]

Srilakshmi S. Pendyala

Investigation being pursued: There are several methods and tools for requirement level verification and validation and architecture specification in the existing literature. Requirement level V&V include analyzing software requirements to determine if they are consistent with, and within the scope of, system requirements, assuring that the requirements are testable and capable of being satisfied. Some of the methods are :

SCR method
Verification and Specification of requirements by 'STATEMATE'
N-Fold inspection
Measuring consensus etc.

Approach to be taken:

I propose to comprehensively study and analyze such methods and compare their applicability for some particular areas like 'ecommerce/web application'.
I will try to identify a suitable problem which can be used to benchmark the performance of all these methods and give a quantitative comparison results.

The list of references:

Tools for formal specification, verification, and validation of requirements Heitmeyer, C. Kirby, J. Labaw, B. Center for High Assurnce Comput. Syst., Naval Res. Lab., Washington, DC;
Formal methods for verification and validation of partial specifications: A case studySteve NASA/WVU Software Research Lab, NASA Independent Verification and Validation Facility, 100 University Drive, Fairmont, WV 26554, USA

[link]