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

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

• 批准号: 0707885
• 负责人: Cormac Flanagan
• 金额: $ 15万
• 依托单位: University of California-Santa Cruz
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-07-15 至 2010-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0707885&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-07701PI(s)：Leavens、Gary T. Cheon、Yoonsik Clifton、Curtis C. Basu、Samik； Rajan, Hridesh 机构：爱荷华州立大学 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)：科马克·弗拉纳根Naumann, David A. Robby 院校：加州大学圣克鲁斯史蒂文斯理工学院 堪萨斯州立大学 圣克鲁斯分校，CA 95064-4107 霍博肯，新泽西州 07030-5991 曼哈顿，堪萨斯州 66506-1103 标题：CRD：Collab Rsch：JML 社区 Infr 振兴工具和辅助正式方法的文档 RschProject 提议：这个合作项目，振兴工具和文档以帮助正式方法研究，旨在。增强 JML 的基础设施，包括其类型检查器、运行时断言检查编译器和 IDE 支持；使JML的软件基础设施更具可扩展性； 。大幅改进该语言及其支持工具的文档； 。开发课程材料和教程，以促进 JML 的课堂使用；和。传播文档齐全、可扩展、开源的增强型 JML 工具套件。JML（Java 建模语言）是一种正式规范语言，可以记录 Java 和接口的详细设计，已在不同的项目中使用，并带来了巨大的好处。用户的反馈是被使用各种工具根据 JML 规范检查 Java 代码的能力所吸引。然而，新的研究问题迫使人们重新发明 JML 提供的基础设施，从而减慢了创新速度，因为 JML 不支持 Java 版本 5 的许多新功能，尤其是泛型。验证软件重大挑战已确定缺乏用于形式方法研究的可扩展工具是实验的主要障碍。该项目通过增强、扩展和详细记录基础设施来应对这一挑战，以推进和加速 Java 形式化方法研究。 更广泛的影响：该基础设施预计将通过赋予大量的共享通用、成熟的规范语言的工具。这些优势应该会吸引更多的教育工作者，并提高安全和关键任务系统的可靠性。此外，加强软件工程课程中的形式方法部分，将开发课程并针对本科生研究。该合作涉及两个少数族裔服务机构和一个 EPSCoR 州的机构。