World Library  
Flag as Inappropriate
Email this Article

Alloy Analyzer

Article Id: WHEBN0000433678
Reproduction Date:

Title: Alloy Analyzer  
Author: World Heritage Encyclopedia
Language: English
Subject: Alloy (specification language), Massachusetts Institute of Technology
Collection: Formal Methods Tools, Massachusetts Institute of Technology, Satisfiability Problems
Publisher: World Heritage Encyclopedia

Alloy Analyzer

Alloy Analyzer.

In computer science and software engineering, the Alloy Analyzer is a software tool which can be used to analyze specifications written in the Alloy specification language.[1] The Analyzer can generate instances of model invariants, simulate the execution of operations defined as part of the model, and check user-specified properties of a model. The Alloy Analyzer supports the analysis of partial models. As a result, it can perform incremental analysis of models as they are constructed, and provide immediate feedback to users.

The Alloy Analyzer, and the associated Alloy language, were developed by a team led by Daniel Jackson at the Massachusetts Institute of Technology in the United States.

Approach to analysis

The Alloy Analyzer was specifically developed to support so-called "lightweight formal methods". As such, it is intended to provide fully automated analysis, in contrast to the interactive theorem proving techniques commonly used with specification languages similar to Alloy. Development of the Analyzer was originally inspired by the automated analysis provided by model checkers. However, model-checking is ill-suited to the kind of models that are typically developed in Alloy, and as a result the core of the Analyzer was eventually implemented as a model-finder built atop a boolean SAT solver.[1]

Through version 3.0, the Alloy Analyzer incorporated an integral SAT-based model-finder based on an off-the-shelf SAT-solver. However, as of version 4.0 the Analyzer makes use of the Kodkod model-finder, for which the Analyzer acts as a front-end. Both model-finders essentially translate a model expressed in relational logic into a corresponding boolean logic formula, and then invoke an off-the-shelf SAT-solver on the boolean formula. In the event that the solver finds a solution, the result is translated back into a corresponding binding of constants to variables in the relational logic model.[2]

In order to ensure the model-finding problem is decidable, the Alloy Analyzer performs model-finding over restricted scopes consisting of a user-defined finite number of objects. This has the effect of limiting the generality of the results produced by the Analyzer. However, the designers of the Alloy Analyzer justify the decision to work within limited scopes through an appeal to the small scope hypothesis:[1] that a high proportion of bugs can be found by testing a program for all test inputs within some small scope.[3]


  1. ^ a b c  
  2. ^ Torlak, E.; Dennis, G. (April 2008). "Kodkod for Alloy Users" (PDF). First ACM Alloy Workshop. Portland, Oregon. Retrieved 2009-04-19. 
  3. ^ Andoni, Alexandr; Daniliuc, Dumitru; Khurshid, Sarfraz; Marinov, Darko (2002). "Evaluating the small scope hypothesis".  

External links

  • The Alloy website at MIT
  • A Guide to Alloy
  • Kodkod analysis engine website at MIT
  • An Alloy Metamodel in Ecore
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from World eBook Library are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.