ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models | SpringerLink
Skip to main content
Springer Nature Link
Log in

ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models

  • Conference paper
Abstract State Machines, Alloy, B and Z (ABZ 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5977))

Included in the following conference series:

  • 686 Accesses

Abstract

Alloy [Jac02a] is a widely adopted relational modeling language. Its appealing syntax and the support provided by the Alloy Analyzer [Jac02b] tool make model analysis accessible to a public of non-specialists. A model and property are translated to a propositional formula, which is fed to a SAT-solver to search for counterexamples. The translation strongly depends on user-provided bounds for data domains called scopes - the larger the scopes, the more confident the user is about the correctness of the model. Due to the intrinsic complexity of the SAT-solving step, it is often the case that analyses do not scale well enough to remain feasible as scopes grow.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Similar content being viewed by others

References

  1. Andersen, H.R., Hulgaard, H.: Boolean expression diagrams. Information and computation 179(2), 194–212 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  2. Eén, N., Sörensson, N.: An extensible sat solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Google Scholar 

  3. Jackson, D.: Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology 11(2), 256–290 (2002)

    Article  Google Scholar 

  4. Jackson, D.: A micromodels of software: Lightweight modelling and analysis with Alloy. Computer Science and Artificial Intelligence Laboratory. MIT, Cambridge (2002)

    Google Scholar 

  5. Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J.: MPI: The complete reference. MIT Press, Cambridge (1998)

    Google Scholar 

  6. Zave, P.: Compositional binding in network domains. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 332–347. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, FCEyN, Universidad de Buenos Aires,  

    Nicolás Rosner, Juan P. Galeotti, Carlos G. Lopez Pombo & Marcelo F. Frias

Authors
  1. Nicolás Rosner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Juan P. Galeotti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Carlos G. Lopez Pombo
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Marcelo F. Frias
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Département d’informatique, Sherbrooke, Université de Sherbrooke, J1K 2R1, Québec, Canada

    Marc Frappier

  2. School of Computing Science, Simon Fraser University, V5A 1S6, Burnaby, BC, Canada

    Uwe Glässer

  3. Department of Electrical and computer Engineering, University of Texas at Austin, 1 University Station C5000, 78712-0240, Austin, TX, USA

    Sarfraz Khurshid

  4. Département informatique, Route forestiére Hurtault, Université Paris-Est Créteil, IUT Sénart/Fontainebleau, 77300, Fontainebelau, France

    Régine Laleau

  5. Department of Computer Science, The University of Waikato, 3240, Hamilton, New Zealand

    Steve Reeves

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rosner, N., Galeotti, J.P., Lopez Pombo, C.G., Frias, M.F. (2010). ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds) Abstract State Machines, Alloy, B and Z. ABZ 2010. Lecture Notes in Computer Science, vol 5977. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11811-1_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11811-1_33

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11810-4

  • Online ISBN: 978-3-642-11811-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation