CRI: CRD -- Development of Alloy Tools, Technology and Materials

提案#：CNS07-07612PI(S)：杰克逊，丹尼尔研究所：麻省理工学院剑桥分校，MA 02139-4307标题：合作RSCH：开发合金工具、技术和材料项目建议：这个合作项目，开发一个新的合金基础设施，旨在进一步开发这种方法。合金，一种建模和分析软件的方法，包括一种语言和一套工具(特别是合金分析器，用于探索和检查软件设计的工具)，结合了一个经典的想法，用关系逻辑表示复杂的系统，以及一个新的想法，使用SAT求解器来探索巨大的案例。合金已被广泛用于各种设计分析中。研究人员使用合金作为工具或他们自己工具的后端；今天有30多门课程使用合金。它最近被用来对电子钱包系统Mondex的传输协议进行建模和检查。25名学生在5年前建造了这台分析仪。然而，基础设施存在严重缺陷，部分原因是其各个组成部分没有完全分开。现在这个分析仪已经变得脆弱和臃肿了。这个基础设施旨在纠正这种情况。它的开发包括：-工具和组件，-教育材料，包括课程模块、案例研究、样本问题和常见模式，以及-社区存储库，允许共享工具、组件、教育材料和研究论文。最终用户应用程序将包括新版本的合金分析器、用于检查代码是否符合合金规范的工具，以及基于实例的建模工具。这些应用程序将构建在所有文档记录的、清晰分离的组件上，这些组件将提供给研究人员：一个除了模型约束之外还可以处理大型配置的新引擎、一个代码前端、一个可视化工具和一个从JML到合金的翻译器。此基础设施旨在创建和支持一个社区，该社区将使用合金作为智能沙盒来探索该领域面临的基本和深远的问题。广泛的影响：由于合金分析仪本身具有具体和即时的视觉反馈，扮演着非常关键但具有建设性的导师的角色，合金特别适合小型大学环境中的正规方法教育。此外，科罗拉多还服务于更大的教育工作者和研究人员群体。

Proposal #: CNS 07-07612PI(s): Jackson, Daniel Institution: Massachussets Institute of Technology Cambridge, MA 02139-4307 Title: CRD: Collab Rsch: Development of Alloy Tools, Technology, and MaterialsProject Proposed:This collaborative project, developing a new Alloy infrastructure, aims to exploit further this approach.Alloy, an approach to modeling and analyzing software that comprises a language and a suite of tools (in particular the Alloy Analyzer, a tool for exploring and checking software designs), brings together a classical idea, the representation of complex systems with relational logic, and a recent idea, the use of SAT solvers for exploring huge cases. Alloy has been used in a wide variety of design analyses. Researchers use Alloy as a tool or back-end for their own tools; over thirty courses use Alloy today. It was recently used to model and check the transfer protocol of Mondex, an electron purse system. Twenty five students built the Analyzer over 5 years ago. However, the infrastructure suffers serious deficiencies, partly due to the fact that its individual components are not cleanly separated. Now this Analyzer has become fragile and bloated. This infrastructure aims to correct this situation. Its development comprises:- Tools and components,- Educational Materials, including course modules, case studies, sample problems, and common patterns, and a - Community Repository, allowing the sharing of tools, components, educational materials, and research papers.End-user applications will include a new version of the Alloy Analyzer, a tool for checking code against Alloy specifications, and an example-based modeling tool. The applications will be built on all-documented, cleanly separated components that will be made available to researchers: a new engine that can handle large configurations in addition to model constraints, a code front-end, a visualizer, and a translator for JML to Alloy. This infrastructure aims to create and enable a community that will use Alloy as an intellectual sandbox to explore fundamental and far-reaching questions faced by the field.Broader Impacts: Because the Alloy Analyzer itself, with its concrete and immediate visual feedback, plays the role of a very critical but constructive tutor, Alloy is particularly well suited to formal methods education in small college settings. Moreover, Alloy serves the larger community of educators and researchers.