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

提案编号：CNS 07-09217 07-07874 07-07701PI(s): Leavens, Gary T. Cheon, Yoonsik Clifton, Curtis C. Basu, Samik；Rajan， hrish机构：爱荷华州立大学UTEP Rose-Hulman Institute Tech Ames， IA 50011-2207 El Paso, TX 79968-0587 Terra Haute， IN 47803-3920提案编号：CNS 07-07885 07-08330 07-09169PI(s): Flanagan, Cormac Naumann, David A. robby机构：UC-Santa Cruz Stevens Institute of Tech Kansas State U Santa Cruz， CA 95064-4107 Hoboken, NJ 07030-5991 Manhattan， KS 66506-1103标题：CRD: Collab rch；JML社区基础设施-振兴工具和文档以帮助正式方法rsch项目建议：这个协作项目，振兴工具和文档以帮助正式方法研究，旨在。增强JML的基础设施，包括类型检查器、运行时断言检查编译器和IDE支持。使JML的软件基础设施更具可扩展性；． 大幅改进该语言及其支持工具的文档；． 开发课程材料和教程，促进课堂使用JML；和。传播一套文档完备的、可扩展的、开源的增强型JML工具。JML （Java建模语言）是一种正式的规范语言，它可以记录Java和接口的详细设计，已经在不同的项目中得到了很好的应用。用户对使用各种工具根据JML规范检查Java代码的能力很感兴趣，因此获得了反馈。然而，新的研究问题迫使重新发明JML提供的基础设施，减缓了创新，因为JML不支持Java版本5的许多新特性，最明显的是泛型。验证软件大挑战已经确定了缺乏可扩展的工具用于正式方法研究，这是实验的主要障碍。该项目通过增强、扩展和良好地记录基础设施来推进和加速Java形式化方法的研究，从而应对了这一挑战。更广泛的影响：基础设施被期望为软件工程专业人员采用正式方法打开障碍，因为它赋予了大量的工具集合，这些工具共享一种通用的、成熟的规范语言。这些优势应该会吸引更多的教育工作者，并提高安全和关键任务系统的可靠性。此外，在软件工程课程中加强形式方法的组成部分，将开发针对本科生研究的课程。该合作涉及两个少数民族服务机构和一个EPSCoR州的机构。

Proposal #: CNS 07-09217 07-07874 07-07701PI(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-3920Proposal #: CNS 07-07885 07-08330 07-09169PI(s): Flanagan, Cormac Naumann, David A. RobbyInstitution: UC-Santa Cruz Stevens Institute of Tech Kansas State U Santa Cruz, CA 95064-4107 Hoboken, NJ 07030-5991 Manhattan, KS 66506-1103Title: CRD: Collab Rsch: JML Community Infr-Revitalizing Tools and Documentation to Aid Formal Methods RschProject 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.