Alloy Analyzer

from Wikipedia, the free encyclopedia
Alloy Analyzer

Screenshot of Alloy Analyzer.png
Screenshots with example
Basic data

Maintainer Daniel Jackson
Current  version 5.1.0
(August 19, 2019)
operating system platform independent
programming language Java
License MIT license
German speaking No
AlloyTools

The Alloy Analyzer is a program used in computer science and software engineering that can be used to analyze and simulate specifications that are written in the Alloy language . The program can generate models of the specification (models in the sense of formal logic ), i.e. instances of all invariants that were defined in the specification. The Alloy language is based on relational logic and is particularly suitable for specifying structures as they often occur in software design , for example architectures, database schemes, network topologies, ontologies, etc. In addition, it is possible in Alloy to include the dimension of time in the specification, so that changes to structures can also be examined through actions.

The Alloy Analyzer supports the incremental development of specifications for such structures by generating models that can be used to check whether the desired properties of the structures are actually met. In this way it is a tool of agile modeling.

The Alloy language and the Alloy Analyzer have been developed since 1997 under the direction of Daniel Jackson at the Massachusetts Institute of Technology in the USA. The designation “alloy” comes from the fact that alloy was influenced by concepts of the specification language Z and model checking .

Analytical approach

The Alloy language has expanded the expressive power of first- order predicate logic to include transitive closure . So it is not decidable. Therefore, a finite size of the universe to be considered is given for the analysis of specifications in the Alloy Analyzer. This has the consequence that the general validity of the results is limited. However, the developers of Alloy Analyzer justify the decision to restrict the scope with reference to the small scope hypothesis , which states that a high proportion of program errors can already be found if the program is checked for all input values ​​of a small scope.

By restricting it to finite universes, a specification in Alloy can be transformed into a formula of propositional logic. In order to find models for the specification, assignments of this formula must then be found. That is, the task of the alloy analyzer can be traced back to the satisfiability problem of propositional logic . Programs that solve the satisfiability problem are called SAT solvers . In the Alloy Analyzer, the Constraint solver Kodkod is used, which transforms the specification in Alloy into the propositional logic and then a SAT solver such as e.g. B. SAT4J to find satisfactory assignments. These are then transformed back into alloy .

Applications

Alloy and the Alloy Analyzer have been used in a wide variety of studies. Examples are:

  • Critical systems , such as in medical technology.
  • Network protocols : Pamela Zave was able to find errors in Chord with the help of the Alloy Analyzer and suggest corrections.
  • Web security : A group at UC Berkeley and Stanford universities used Alloy and the Alloy Analyzer to examine various aspects of web security.
  • Code Verification : Greg Dennis developed a tool called Forge that uses Alloy and can validate Java code annotated with specifications from the Java Modeling Language JML. This tool was used to verify Java libraries and the code of an electronic voting system.

Individual evidence

  1. ^ A b c Daniel Jackson: Software Abstrations: Logic, Language, and Analysis . MIT Press , 2012, ISBN 978-0-262-01715-2 .
  2. ↑ Alexandr Andoni, Dumitru Daniliuc, Sarfraz Khurshid and Darko Marinov (2002), " Evaluating the small scope hypothesis "
  3. ↑ University of Washington PLSE neutron , UW PLSE neutron
  4. ↑ Pamela Zave: Reasoning about identifier spaces: How to make Chord correct, in: IEEE Trans. Software Engineering 43 , 12 (Dec. 2017), 1144–1156.
  5. ↑ Akhawe, D., Barth, A., Lam, PE, Mitchell, J. and Song, D .: Towards a formal foundation of Web security, in: Proceedings of the 23rd IEEE Computer Security Foundations Symp. Edinburgh, 2010, 290 -304.
  6. ↑ Dennis, G., Chang, F. and Jackson, D .: Modular verification of code with SAT, in: Proceedings of the Intern. Symp. Software Testing and Analysis , Portland, ME, July 2006.
  7. ↑ Dennis, G., Yessenov, K. and Jackson, D .: Bounded verification of voting software, in: Proceedings of the 2nd IFIP Working Conf. Verified Software: Theories, Tools, and Experiments . Toronto, Oct. 2008.

Web links