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.
