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

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

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.