Bounded Model Checking of Temporal Formulas with Alloy

  • Alcino Cunha
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8477)


Alloy is a formal modeling language based on first-order relational logic, with no native support for specifying reactive systems. We propose an extension of Alloy to allow the specification of temporal formulas using LTL, and show how they can be verified by bounded model checking with the Alloy Analyzer.


Model Check Linear Temporal Logic Execution Trace Liveness Property Alloy Analyzer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Chang, F., Jackson, D.: Symbolic model checking of declarative relational models. In: ICSE, pp. 312–320. ACM (2006)Google Scholar
  3. 3.
    Frias, M., Galeotti, J., Pombo, C., Aguirre, N.: DynAlloy: upgrading Alloy with actions. In: ICSE, pp. 442–451. ACM (2005)Google Scholar
  4. 4.
    Immerman, N., Vardi, M.: Model checking and transitive-closure logic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 291–302. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  5. 5.
    Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press (2012) (revised edition)Google Scholar
  6. 6.
    Near, J.P., Jackson, D.: An imperative extension to Alloy. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 118–131. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. 7.
    Vakili, A., Day, N.A.: Temporal logic model checking in Alloy. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 150–163. Springer, Heidelberg (2012)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Alcino Cunha
    • 1
  1. 1.HASLab – High Assurance Software LaboratoryINESC TEC & Universidade do MinhoBragaPortugal

Personalised recommendations