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

Massachusetts Institute Of Technology, Cambridge MA

Investigators

Abstract

Proposal #: CNS 07-07612 PI(s): Jackson, Daniel Institution: Massachussets Institute of Technology Cambridge, MA 02139-4307 Title: CRD: Collab Rsch: Development of Alloy Tools, Technology, and Materials Project 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.