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

提案#：CNS07-09217 07-07874 07-07701PI(S)：Leaven，Gary T.Cheon，Yoonsik Clifton，Curtis C.Basu，Samik；建议编号：CNS07-07885 07-08330 07-09169PI(S)：弗拉纳根，科马克·瑙曼，大卫·A·罗比研究所：加州大学圣克鲁斯分校史蒂文斯理工学院堪萨斯州立大学圣克鲁斯州立U Santa Cruz，CA 95064-4107 Hoboken，NJ 07030-5991曼哈顿，KS 66506-1103TITLE：CRD：Colrsch：JML社区重建工具和文档以援助正式方法Rschby项目建议：该合作项目，振兴工具和文件，以帮助正式方法研究，旨在。增强JML的基础设施，包括其类型检查器、运行时断言检查编译器和IDE支持；使JML的软件基础设施更具可扩展性；大大改进该语言及其辅助工具的文件编制工作；编写课程材料和教程，以促进JML的课堂使用；以及发布文档齐全、可扩展、开源的增强JML工具套件。JML(Java建模语言)是一种正式的规范语言，可以记录Java和接口的详细设计，已在不同的项目中使用并带来了巨大的好处。反馈来自用户，他们被使用各种工具检查Java代码与JML规范的能力所吸引。然而，新的研究问题正在迫使重新发明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.