Alcoa: the alloy constraint analyzer

ABSTRACT

Alcoa is a tool for analyzing object models. It has a range of uses. At one end, it can act as a support tool for object model diagrams, checking for consistency of multiplicities and generating sample snapshots. At the other end, it embodies a lightweight formal method in which subtle properties of behaviour can be investigated.Alcoa's input language, Alloy, is a new notation based on Z. Its development was motivated by the need for a notation that is more closely tailored to object models (in the style of UML), and more amenable to automatic analysis. Like Z, Alloy supports the description of systems whose state involves complex relational structure. State and behavioural properties are described declaratively, by conjoining constraints. This makes it possible to develop and analyze a model incrementally, with Alcoa investigating the consequences of whatever constraints are given.Alcoa works by translating constraints to boolean formulas, and then applying state-of-the-art SAT solvers. It can analyze billions of states in seconds.

REFERENCES

• 1: Sten Agerholm , Peter Gorm Larsen, The IFAD VDM Tools: Lightweight Formal Methods, Proceedings of the International Workshop on Current Trends in Applied Formal Method: Applied Formal Methods, p.326-329, October 07-09, 1998
• 2: R.J. Bayardo Jr. & R. C. Schrag. Using CSP look-back techniques to solve real world SAT instances. Proc. of the 14th National Conf. on Artificial Intelligence, 203-208, 1997.
• 3: Dan Craigen, Irwin Meisels, and Mark Saaltink. Analysing Z Specifications with Z/EVES. In Industrial-Strength Formal Methods in Practice, J.P. Bowen and M.G. Hinchey (Editors), September 1999.
• 4: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 5: Stephen J. Garland & John V. Guttag, A Guide to LP: the Larch Prover, MIT Laboratory for Computer Science, December 1991. Also available as Research Report 82, Compaq Systems Research Center, Palo Alto, CA.
• 6: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 7: Joseph B. Irineo. An Object-Oriented, Maximum-Likelihood Parameter Estimation Program for GARCH(p,q). Masters Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, June 1999.
• 8: Daniel Jackson. Alloy: A Lightweight Object Modelling Notation. Technical Report 797, MIT Laboratory for Computer Science, Cambridge, MA, February 2000.
• 9: Daniel Jackson. An Automatic Analysis for a First-Order Relational Logic. Submitted for publication. Available at: http://sdg.lcs.mit.edu/~dnj/publications.
• 10: Daniel Jackson, An intermediate design language and its analysis, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.121-130, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 11: Daniel Jackson , Craig A. Damon, Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector, IEEE Transactions on Software Engineering, v.22 n.7, p.484-495, July 1996 [doi>10.1109/32.538605]
• 12: Daniel Jackson, Yuchung Ng and Jeannette Wing. A Nitpick Analysis of IPv6. To appear, Formal Aspects of Computing.
• 13: Daniel Jackson & Mandana Vaziri. Finding Bugs in Code using a Relational Constraint Solver. Submitted for publication. Available at: http://sdg.lcs.mit.edu/~dnj/publications.
• 14: Seung (Albert) Lee. Object Modelling Applied to CTAS. Masters thesis Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, June 1999.
• 15: Barbara Liskov , John Guttag, Program Development in Java: Abstraction, Specification, and Object-Oriented Design, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 16: Logica UK Ltd. Formaliser: A Specification Support Tool. Information at http://www.16.com/offerings/Formaliser.html.
• 17: Sam Owre , John Rushby , Natarajan Shankar , Friedrich von Henke, Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS, IEEE Transactions on Software Engineering, v.21 n.2, p.107-125, February 1995 [doi>10.1109/32.345827]
• 18: J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
• 19: Kevin J. Sullivan , John Socha , Mark Marchukov, Using formal methods to reason about architectural standards, Proceedings of the 19th international conference on Software engineering, p.503-513, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253433]
• 20: Jos Warmer , Anneke Kleppe, The object constraint language: precise modeling with UML, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1998
• 21: Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages
      D.2.4 Software/Program Verification
          Subjects: Model checking

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages, Performance, Reliability, Theory

Keywords:
constraint satisfaction, formal specifications, model checking, object models, relational logic, software analysis