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

提案号：CNS 07-07612PI(s): Jackson， Daniel机构：麻省理工学院剑桥，MA 02139-4307标题：CRD：合作研究：合金工具，技术和材料的发展项目建议：该合作项目，开发新的合金基础设施，旨在进一步利用这种方法。Alloy是一种建模和分析软件的方法，它包括一种语言和一套工具（特别是Alloy Analyzer，一种用于探索和检查软件设计的工具），它结合了一个经典的思想，即用关系逻辑表示复杂系统，以及一个最近的想法，即使用SAT求解器来探索大型案例。合金已广泛应用于各种设计分析。研究人员使用Alloy作为他们自己的工具的工具或后端；今天有30多个课程使用Alloy。它最近被用于模拟和检查电子钱包系统Mondex的传输协议。25名学生在5年前建造了分析仪。然而，基础设施存在严重缺陷，部分原因是其各个组件没有完全分离。现在这个分析器变得脆弱和臃肿。该基础设施旨在纠正这种情况。它的开发包括：-工具和组件，-教育材料，包括课程模块，案例研究，示例问题和通用模式，以及-社区存储库，允许共享工具，组件，教育材料和研究论文。最终用户应用程序将包括一个新版本的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.