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.cite book|last=Jackson|first=Daniel |authorlink=Daniel Jackson (computer scientist)|title = Software Abstractions: Logic, Language, and Analysis|publisher=MIT Press|year = 2006 |id=ISBN 978-0-262-10114-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.

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. [cite conference|first=E. |last=Torlak|coauthors= G. Dennis| title= Kodkod for Alloy Users|booktitle= First ACM Alloy Workshop|location= Portland, Oregon| url= http://web.mit.edu/emina/www/papers/kk4a.pdf| month=November | year=2006| accessdate=2007-05-16|format=PDF]

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": that a high proportion of bugs can be found by testing a program for all test inputs within some small scope. [cite paper|author = Alexandr Andoni, Dumitru Daniliuc, Sarfraz Khurshid, and Darko Marinov | title = Evaluating the small scope hypothesis |url = http://citeseer.ist.psu.edu/623993.html | year=2002]

References

External links

* [http://alloy.mit.edu/alloy4/ The Alloy Analyzer website] at MIT
* [http://www.doc.ic.ac.uk/project/2007/271j/g06271j01/Web/ A Guide to Alloy]
* [http://web.mit.edu/emina/www/kodkod.html Kodkod analysis engine website] at MIT


Wikimedia Foundation. 2010.

Игры ⚽ Поможем решить контрольную работу

Look at other dictionaries:

  • Alloy Analyzer — Alloy Analyser Screenshots mit Beispiel Basisdaten Maintainer Daniel Jackson Aktuel …   Deutsch Wikipedia

  • Alloy — bezeichnet: Alloy Analyzer, ein in der Informatik und Softwaretechnik eingesetztes Programm Alloy Creek, ein Fluss im US Bundesstaat Montana Diese Seite ist eine Begriffsklärung zur Unterscheidung mehrerer mit demselben Wort bezeichneter Begriffe …   Deutsch Wikipedia

  • Alloy (specification language) — In computer science and software engineering, the Alloy specification language is a declarative language for expressing complex structural constraints and behavior in a software system. Alloy provides a simple structural modeling tool based on… …   Wikipedia

  • Формальные методы — Пример формальной спецификации с использованием Z нотации В информатике и инженерии программного обеспечения формальными методами называется группа техник, основанных на математическом аппарате для …   Википедия

  • Daniel Jackson (computer scientist) — Daniel Jackson (born 1963) is a Professor of Computer Science at the Massachusetts Institute of Technology (MIT). He is the principal designer of the Alloy modelling language, and author of the book Software Abstractions: Logic, Language, and… …   Wikipedia

  • 7439-92-1 — Plomb Pour les articles homonymes, voir Plomb (homonymie) et Pb.  Pour l’article homophone, voir Plon …   Wikipédia en Français

  • Plomb — Pour les articles homonymes, voir Plomb (homonymie) et Pb.  Pour l’article homophone, voir Plon …   Wikipédia en Français

  • Corrosion — v · d · e Materials failure modes Buckling · …   Wikipedia

  • ISS-Expedition 8 — Missionsemblem Missionsdaten Mission: ISS Expedition 8 Besatzung: 2 Rettungsschiffe …   Deutsch Wikipedia

  • X-ray photoelectron spectroscopy — [ right|thumb|350px|Basic components of a monochromatic XPS system.] X ray photoelectron spectroscopy (XPS) is a quantitative spectroscopic technique that measures the elemental composition, empirical formula, chemical state and electronic state… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”