Hostname: page-component-7b7567c8c-tnzcf Total loading time: 0 Render date: 2026-11-12T08:00:23.368Z Has data issue: false hasContentIssue false
  • English
  • Français

Applications and extensions of Alloy: past, present and future

Published online by Cambridge University Press:  08 July 2013

EMINA TORLAK,
MANA TAGHDIRI,
GREG DENNIS and
JOSEPH P. NEAR
EMINA TORLAK
Affiliation:
University of California, Berkeley, U.S.A. Email: emina@eecs.berkeley.edu
MANA TAGHDIRI
Affiliation:
Karlsruhe Institute of Technology, Karlsruhe, Germany Email: taghdiri@ira.uka.de
GREG DENNIS
Affiliation:
Google, Cambridge, MA., U.S.A. Email: gdennis@alum.mit.edu
JOSEPH P. NEAR
Affiliation:
Computer Science and Artificial Intelligence Laboratory, MIT, Cambridge, MA., U.S.A. Email: jnear@csail.mit.edu
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Alloy is a declarative language for lightweight modelling and analysis of software. The core of the language is based on first-order relational logic, which offers an attractive balance between analysability and expressiveness. The logic is expressive enough to capture the intricacies of real systems, but is also simple enough to support fully automated analysis with the Alloy Analyzer. The Analyzer is built on a SAT-based constraint solver and provides automated simulation, checking and debugging of Alloy specifications. Because of its automated analysis and expressive logic, Alloy has been applied in a wide variety of domains. These applications have motivated a number of extensions both to the Alloy language and to its SAT-based analysis. This paper provides an overview of Alloy in the context of its three largest application domains, lightweight modelling, bounded code verification and test-case generation, and three recent application-driven extensions, an imperative extension to the language, a compiler to executable code and a proof-capable analyser based on SMT.

References

Abdul Khalek, S. and Khurshid, S. (2010) Automated SQL query generation for systematic testing of database engines. In: ASE 10, Proceedings of the IEEE/ACM International Conference on Automated Software Engineering, ACM 329–332.CrossRefGoogle Scholar
Abrial, J.-R. (1996) The B-Book: Assigning Programs to Meanings, Cambridge University Press.CrossRefGoogle Scholar
Arkoudas, K. (2000) Denotational Proof Languages, Ph.D. thesis, Massachusetts Institute of Technology.Google Scholar
Arkoudas, K., Khurshid, S., Marinov, D. and Rinard, M. (2003) Integrating model checking and theorem proving for relational reasoning. In: Berghammer, R., Möller, B. and Struth, G. (eds.) Relational and Kleene-Algebraic Methods in Computer Science. Springer-Verlag Lecture Notes in Computer Science 3051 21–33.CrossRefGoogle Scholar
Biere, A., Cimatti, A., Clarke, E. M. and Zhu, Y. (1999) Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) TACAS'99. International Journal on Software Tools for Technology Transfer 3 (3)193–207.Google Scholar
Blanchette, J. and Nipkow, T. (2009) Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: TAP 2009: short papers. Technical report tr630, ETH Zurich.CrossRefGoogle Scholar
Bonacina, M. P., Lynch, C. and Moura, L. (2009) On deciding satisfiability by DPLL and unsound theorem proving. In: Schmidt, R. (ed.) Automated Deduction – CADE-22. Springer-Verlag Lecture Notes in Computer Science 5663 35–50.CrossRefGoogle Scholar
Chang, F. (2007) Alloy analyzer 4.0. (Available at http://Alloy.mit.edu/Alloy4/.)Google Scholar
Chen, P. P.-S. (1976) The entity-relationship model – toward a unified view of data. ACM Transactions on Database Systems 1 (1)9–36.CrossRefGoogle Scholar
Dennis, G. (2009) A relational framework for bounded program verification, Ph.D. thesis, Massachusetts Institute of Technology.Google Scholar
Dennis, G., Chang, F. and Jackson, D. (2006) Modular verification of code. In: ISSTA '06: Proceedings of the 2006 International Symposium on Software Testing and Analysis, ACM 109–120.CrossRefGoogle Scholar
Dennis, G., Seater, R., Rayside, D. and Jackson, D. (2004) Automating commutativity analysis at the design level. In: ISSTA '04 – Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ACM 165–174.Google Scholar
Dolby, J., Vaziri, M. and Tip, F. (2007) Finding bugs efficiently with a SAT solver. In: ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT symposium on the Foundations of Software Engineering, ACM 195–204.CrossRefGoogle Scholar
Dougherty, D. J. (2009) An improved algorithm for generating database transactions from relational algebra specifications. In: Mackie, I. and Martins Moreira, A. (eds.) Proceedings Tenth International Workshop on Rule-Based Programming: Rule '09. Electronic Proceedings in Theoretical Computer Science 21 77–89.CrossRefGoogle Scholar
El-Ghazi, A. A. and Taghdiri, M. (2011) Relational reasoning via SMT solving. In: Butler, M. and Schulte, W. (eds.) Proceedings of the 17th International Conference on Formal Methods: FM '11. Springer-Verlag Lecture Notes in Computer Science 6664 133–148.CrossRefGoogle Scholar
Frappier, M., Fraikin, B., Chossart, R., Chane-Yack-Fa, R. and Ouenzar, M. (2010) Comparison of model checking tools for information systems. In: Dong, J. and Zhu, H. (eds.) Formal Methods and Software Engineering: Proceedings ICFEM '10. Springer-Verlag Lecture Notes in Computer Science 6447 581–596.CrossRefGoogle Scholar
Frias, M. F., Galeotti, J. P., López Pombo, C. G. and Aguirre, N. M. (2005) DynAlloy: upgrading Alloy with actions. In: Proceedings of the 27th International Conference on Software Engineering – ICSE '05, ACM 442–451.Google Scholar
Frias, M. F., Pombo, C. G. L. and Moscato, M. M. (2007) Alloy Analyzer+PVS in the analysis and verification of Alloy specifications. In: Grumberg, O. and Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: Proceedings TACAS 2007. Springer-Verlag Lecture Notes in Computer Science 4424 587–601.CrossRefGoogle Scholar
Gal, E. and Toledo, S. (2005) Algorithms and data structures for flash memories. ACM Computing Surveys 37 138–163.CrossRefGoogle Scholar
Galeotti, J., Rosner, N., Pombo, C. and Frias, M. (2010) Analysis of invariants for efficient bounded verification. In: Proceedings of the 19th International Symposium on Software Testing and Analysis – ISSTA '10 25–36.CrossRefGoogle Scholar
Galeotti, J. P. (2010) Software Verification using Alloy, Ph.D. thesis, University of Buenos Aires.Google Scholar
Garavel, H., Mateescu, R., Lang, F. and Serwe, W. (2007) CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W. and Hermanns, H. (eds.) Computer Aided Verification: Proceedings 19th International Conference, CAV 2007. Springer-Verlag Lecture Notes in Computer Science 4590 158–163.CrossRefGoogle Scholar
Gassend, B., Dijk, M. V., Clarke, D., Torlak, E., Devadas, S. and Tuyls, P. (2008) Controlled physical random functions and applications. ACM Transactions on Information and System Security 10 (3)1–22.CrossRefGoogle Scholar
Ge, Y., Barrett, C. and Tinelli, C. (2009) Solving quantified verification conditions using satisfiability modulo theories. Annals of Mathematics and Artificial Intelligence 55 (1)101–122.CrossRefGoogle Scholar
Ge, Y. and Moura, L. (2009) Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A. and Maler, O. (eds.) Computer Aided Verification – Proceedings 21st International Conference, CAV 2009. Springer-Verlag Lecture Notes in Computer Science 5643 306–320.CrossRefGoogle Scholar
Hammer, M. and McLeod, D. (1978) The semantic data model: a modelling mechanism for data base applications. In: Proceedings of the 1978 ACM SIGMOD International Conference on Management of Data, ACM 26–36.CrossRefGoogle Scholar
Holzmann, G. J. (2004) The Spin model checker, Addison-Wesley.Google Scholar
Hynix Semiconductor et al. (2006) Open NAND flash interface specification. Technical report, ONFi Workgroup.Google Scholar
Ives, B. and Earl, M. (1997) Mondex international: Reengineering money. Technical Report CRIM CS97/2, London Business School.Google Scholar
Jackson, D. (2006) Software Abstractions: logic, language, and analysis, MIT Press.Google Scholar
Kang, E. and Jackson, D. (2008) Formal modeling and analysis of a flash filesystem in Alloy. In: Börger, E., Butler, M., Bowen, J. P. and Boca, P. (eds.) Abstract State Machines, B and Z – Proceedings First International Conference, ABZ 2008. Springer-Verlag Lecture Notes in Computer Science 5238 294–308.CrossRefGoogle Scholar
Kang, E. and Jackson, D. (2009) Designing and analyzing a flash file system with Alloy. International Journal of Software and Informatics 3 (2)129–148.Google Scholar
Khalek, S., Elkarablieh, B., Laleye, Y. and Khurshid, S. (2008) Query-aware test generation using a relational constraint solver. In: Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering: ASE '08, IEEE Computer Society 238–247.Google Scholar
Krishnamurthi, S., Fisler, K., Dougherty, D. J. and Yoo, D. (2008) Alchemy: transmuting base Alloy specifications into implementations. In: SIGSOFT '08/FSE-16: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, ACM 158–169.CrossRefGoogle Scholar
Leuschel, M. and Butler, M. J. (2003) ProB: A model checker for B. In: Araki, K., Gnesi, S. and Mandrioli, D. (eds.) Proceedings FME 2003: Formal Methods. Springer-Verlag Lecture Notes in Computer Science 2805 855–874.CrossRefGoogle Scholar
Manson, J., Pugh, W. and Adve, S. V. (2005) The Java memory model. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages: POPL '05, ACM 378–391.CrossRefGoogle Scholar
Marinov, D. and Khurshid, S. (2001) Testera: A novel framework for automated testing of Java programs. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering: ASE '01, IEEE Computer Society 22.Google Scholar
Momtahan, L. (2005) Towards a small model theorem for data independent systems in Alloy. Electronic Notes in Theoretical Computer Science 128 (6)37–52.CrossRefGoogle Scholar
Narain, S., Levin, G., Kaul, V. and Malik, S. (2008) Declarative infrastructure configuration synthesis and debugging. Journal of Network and Systems Management 16 (3)235–258.CrossRefGoogle Scholar
Near, J. P. (2010) From relational specifications to logic programs. In: Hermenegildo, M. and Schaub, T. (eds.) Technical Communications of the 26th International Conference on Logic Programming: ICLP '10. Leibniz International Proceedings in Informatics 7 144–153.Google Scholar
Near, J. P. and Jackson, D. (2010) An imperative extension to Alloy. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R. and Reeves, S. (eds.) Abstract State Machines, Alloy, B and Z Second International Conference, ABZ 2010. Springer-Verlag Lecture Notes in Computer Science 5977 118–131.CrossRefGoogle Scholar
Owre, S., Shankar, N. and Rushby, J. (1992) PVS: A prototype verification system. In: Kapur, D. (ed.) Automated Deduction – CADE-11: Proceedings 11th International Conference on Automated Deduction. Springer-Verlag Lecture Notes in Computer Science 607 748–752.CrossRefGoogle Scholar
Ramananandro, T. (2008) Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method. Formal Aspects of Computing 20 (1)21–39.CrossRefGoogle Scholar
de la Riva, C., Suárez-Cabal, M. J. and Tuya, J. (2010) Constraint-based test database generation for SQL queries. In: Proceedings of the 5th Workshop on Automation of Software Test: AST '10, ACM 67–74.CrossRefGoogle Scholar
Roscoe, B. (2005) The Theory and Practice of Concurrency, Prentice Hall, 3rd edition.Google Scholar
Sakai, M. and Imai, T. (2009) CForge: A bounded verifier for the C language. In: The 11th Programming and Programming Language workshop (PPL '09).Google Scholar
Seater, R., Jackson, D. and Gheyi, R. (2007) Requirement progression in problem frames: deriving specifications from requirements. Requirements Engineering Journal 12 (2)77–102.CrossRefGoogle Scholar
Ševčík, J. and Aspinall, D. (2008) On validity of program transformations in the Java memory model. In: Vitek, J. (ed.) ECOOP 2008 – Object-Oriented Programming: Proceedings 22nd European Conference. Springer-Verlag Lecture Notes in Computer Science 5142 27–51.CrossRefGoogle Scholar
Shao, D., Khurshid, S. and Perry, D. (2007) Whispec: White-box testing of libraries using declarative specifications. In: Proceedings of the 2007 Symposium on Library-Centric Software Design – LCSD '07, ACM 11–20.CrossRefGoogle Scholar
Spiridonov, A. and Khurshid, S. (2007) Pythia: Automatic generation of counterexamples for ACL2 using Alloy. In: Proceedings of the 7th International Workshop on the ACL2 Theorem Prover and its Applications.Google Scholar
Spivey, J. M. (1992) The Z Notation: A Reference Manual, International Series in Computer Science, Prentice Hall.Google Scholar
Stepney, S., Cooper, D. and Woodcock, J. (2000) An electronic purse: Specification, refinement and proof. Technical report, Oxford University Computing Laboratory, Programming Research Group.Google Scholar
Taghdiri, M. (2007) Automating Modular Program Verification by Refining Specifications, Ph.D. thesis, Massachusetts Institute of Technology.Google Scholar
Taghdiri, M. and Jackson, D. (2003) A lightweight formal analysis of a multicast key management scheme. In: König, H., Heiner, H. and Wolisz, A. (eds.) Formal Techniques for Networked and Distributed Systems – FORTE 2003: Proceedings 23rd IFIP WG 6.1 International Conference. Springer-Verlag Lecture Notes in Computer Science 2767 240–256.CrossRefGoogle Scholar
Taghdiri, M. and Jackson, D. (2007) Inferring specifications to detect errors in code. Journal of Automated Software Engineering 14 (1)87–121.CrossRefGoogle Scholar
Taghdiri, M., Seater, R. and Jackson, D. (2006) Lightweight extraction of syntactic specifications. In: SIGSOFT '06/FSE-14: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering 276–286.CrossRefGoogle Scholar
The Open Group (2003) The POSIX 1003.1, 2003 edition specification. (Available at: http://www.opengroup.org/certification/idx/posix.html.)Google Scholar
Torlak, E. (2009) A constraint solver for software engineering: finding models and cores of large relational specifications, Ph.D. thesis, MIT.Google Scholar
Torlak, E., Chang, F. and Jackson, D. (2008) Finding minimal unsatisfiable cores of declarative specifications. In: Cuellar, J., Maibaum, T. and Sere, K. (eds.) FM 2008: Formal Methods – Proceedings 15th International Symposium on Formal Methods. Springer-Verlag Lecture Notes in Computer Science 5014 326–341.CrossRefGoogle Scholar
Torlak, E. and Jackson, D. (2007) Kodkod: A relational model finder. In: Grumberg, O. and Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: Proceedings TACAS 2007. Springer-Verlag Lecture Notes in Computer Science 4424 632–647.CrossRefGoogle Scholar
Torlak, E., Vaziri, M. and Dolby, J. (2010) Memsat: checking axiomatic specifications of memory models. In: PLDI '10 – Proceedings of the 2010 ACM SIGPLAN conference on Programming Language Design and Implementation. ACM SIGPLAN Notices 45 (6)341–350.CrossRefGoogle Scholar
Tuya, J., Suárez-Cabal, M. J. and de la Riva, C. (2010) Full predicate coverage for testing SQL database queries. Software Testing, Verification and Reliability 20 (3)237–288.CrossRefGoogle Scholar
Uzuncaova, E., Garcia, D., Khurshid, S. and Batory, D. (2008) Testing software product lines using incremental test generation. In: ISSRE '08 Proceedings of the 2008 19th International Symposium on Software Reliability Engineering, IEEE Computer Society 249–258.Google Scholar
Uzuncaova, E. and Khurshid, S. (2008) Constraint prioritization for efficient analysis of declarative models. In: Cuellar, J., Maibaum, T. and Sere, K. (eds.) FM 2008: Formal Methods, Proceedings 15th International Symposium on Formal Methods. Springer-Verlag Lecture Notes in Computer Science 5014 310–325.CrossRefGoogle Scholar
Vaziri, M. (2004) Finding Bugs in Software with a Constraint Solver, Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA.Google Scholar
Wang, H. H., Dong, J. S., Sun, J. and Sun, J. S. (2006) Reasoning support for semantic web ontology family languages using Alloy. Multiagent and Grid Systems 2 (4)455–471.CrossRefGoogle Scholar
Yeung, V. (2006) Declarative configuration applied to course scheduling. Master's thesis, Massachusetts Institute of Technology, Cambridge, MA.Google Scholar