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

协作研究：CRI：CRD：JML 社区基础设施——振兴工具和文档以帮助形式化方法研究

• 批准号: 0808913
• 负责人: Gary Leavens
• 金额: --
• 依托单位: The University of Central Florida Board of Trustees
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-09-28 至 2010-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0808913&HistoricalAwards=false
• 关键词: Collaborative; Research; CRI; CRD; JML

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.

提案编号：CNS 07-09217 07-07874 07- 07701 PI（s）： Leavens，加里T. 放大图片作者：Yoonsik克利夫顿，Curtis C. 研究机构：爱荷华州州立大学UTEP Rose-Hulman Institute Tech艾姆斯，IA 50011-2207 El Paso，TX 79968-0587 Terra Haute，IN 47803- 3920提案编号：CNS 07-07885 07-08330 07- 09169 PI（s）： 放大图片作者：Cormac Naumann，大卫A. Robby机构：UC-Santa Cruz Stevens Institute of Tech堪萨斯州立大学圣克鲁斯，CA 95064-4107 Hoboken，NJ 07030-5991曼哈顿，KS 66506- 1103标题：CRD：Collab Rsch：JML Community Infr-Revitalizing Tools and Documentation to Aid Formal Methods Rsch项目建议：这个合作项目，振兴工具和文档以帮助正式方法研究，旨在。增强JML的基础设施，包括类型检查器、运行时断言检查编译器和IDE支持;使JML的软件基础设施更具可扩展性;大大改进该语言的文档及其支持工具;开发课程材料和教程，以促进JML的课堂使用;以及。JML（Java Modeling Language，Java建模语言）是一种正式的规范语言，它可以记录Java和接口的详细设计，已经在不同的项目中得到了很好的应用。反馈来自用户，他们被使用各种工具根据JML规范检查Java代码的能力所吸引。然而，新的研究问题迫使重新发明JML提供的基础设施，减缓了创新，因为JML不支持Java版本5的许多新功能，最明显的是泛型。验证软件的大挑战已经确定缺乏可扩展的工具，正式的方法研究作为一个主要的障碍实验。这个项目响应的挑战，通过增强，扩展和良好的记录的基础设施，以推进和加速Java正式的方法research.Broader的影响：基础设施预计将开放的障碍，正式的方法采用软件工程专业人士赋予一个大的工具集合，共享一个共同的，成熟的规范语言。这些优势将吸引更多的教育工作者，并提高安全和任务关键型系统的可靠性。此外，在软件工程课程中加强形式方法的内容，将课程开发和针对本科生的研究，。该合作涉及两个少数民族服务机构和一个EPSCoR州的机构。