Graduate Topics for CS 378/395T

Neha Agrawal

[link]

Ashwini S. Athalye

[link]

Namrata L. Baliga, Nupur C. Kulkarni

[link]

Pranav D. Bhandarkar

[link]

Aparna Boddupalli, Aarthi Ganesan

[link]

Chester Warren Hoster

[link]

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:

  1. A survey of the Java Pathfinder and Pathexplorer tools.
  2. Architecture of Java Pathfinder
  3. How JPF translates Java to Promela (language used by SPIN), A survey of SPIN model checker and how SPIN and JPF work together.
  4. A case study of the application of JPF to find errors in NASA's remote agent space craft controller
  5. 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 :

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

Approach to be taken:

The list of references:

[link]

Yu-Ting Peng

[link]

Neelima Premsankar

[link]

Saurabh Subodh Shukla

[link]

DongJin Suh

[link]

Dongliang Xu

[link]