Collaborative Research: CRI: CRD: A JML Community Infrastructure --Revitalizing Tools and Documentation to Aid Formal Methods Research

Proposal #: CNS 07-09217 07-07874 07-07701

PI(s): Leavens, Gary T. Cheon, Yoonsik Clifton, Curtis C.

Basu, Samik; Rajan, Hridesh

Institution: Iowa State University UTEP Rose-Hulman Institute Tech

Ames, IA 50011-2207 El Paso, TX 79968-0587 Terra Haute, IN 47803-3920

Proposal #: CNS 07-07885 07-08330 07-09169

PI(s): Flanagan, Cormac Naumann, David A. Robby

Institution: UC-Santa Cruz Stevens Institute of Tech Kansas State U

Santa Cruz, CA 95064-4107 Hoboken, NJ 07030-5991 Manhattan, KS 66506-1103

Title: CRD: Collab Rsch: JML Community Infr-Revitalizing Tools and Documentation to Aid Formal Methods Rsch

Project Proposed:

This collaborative project, revitalizing tools and documentations to aid formal methods research, aims to

. Enhance JML's infrastructure including its type checker, runtime assertion checking compiler, and IDE support;

. Make JML's software infrastructure more extensible;

. Substantially improve the documentation of the language and its supporting tools;

. Develop course materials and tutorials to facilitate classroom use of JML; and

. Disseminate a well-documented, extensible, open source suite of enhanced JML tools.

JML (Java Modeling Language), a formal specification language that can document detailed designs of Java and interfaces, has been used in different projects with great benefit. Feedback is obtained from users who are attracted by the ability to check Java code against JML specifications using a variety of tools. New research problems, however, are forcing re-inventing the infrastructure that JML provides, slowing the innovation, since JML does not support many of the new features of Java version 5, most notably generics. The Verified Software grand challenge has identified lack of extensible tools for formal methods research as a major impediment to experimentation. This project responds to the challenge by enhancing, extending, and well-documenting the infrastructure to advance and accelerate Java formal methods research.

Broader Impacts: The infrastructure is expected to open barriers to formal methods adoption among software engineering professionals by endowing a large collection of tools that share a common, mature specification language. These advantages should attract more educators and improve reliability in safety- and mission-critical systems. Moreover, strengthening the formal methods component in software engineering curriculum, courses will be developed and targeted to undergraduate research,. The collaborative involves two minority-serving institutions and an institution in an EPSCoR state.