skip to main content
research-article

Efficient Analysis of DynAlloy Specifications

Published: 12 December 2007 Publication History

Abstract

DynAlloy is an extension of Alloy to support the definition of actions and the specification of assertions regarding execution traces. In this article we show how we can extend the Alloy tool so that DynAlloy specifications can be automatically analyzed in an efficient way. We also demonstrate that DynAlloy's semantics allows for a sound technique that we call program atomization, which improves the analyzability of properties regarding execution traces by considering certain programs as atomic steps in a trace.
We present the foundations, case studies, and empirical results indicating that the analysis of DynAlloy specifications can be performed efficiently.

References

[1]
Alpern, B. and Schneider, F. B. 1985. Defining liveness. Inform. Proc. Lett. 21, 4, 181--185.
[2]
Dijkstra, E. W. and Scholten, C. S. 1990. Predicate Calculus and Program Semantics. Springer-Verlag, New York, NY.
[3]
Floyd, R. W. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics. American Mathematical Society, Providence, Rhode Island, pp. 19--32.
[4]
Frias, M. F., Galeotti, J. P., Lopez Pombo, C. G., and Aguirre, N. M. 2005a. DynAlloy: upgrading alloy with actions. In Proceedings of the 27th International Conference on Software Engineering, G.-C. Roman, Ed. Association for Computing Machinery and IEEE Computer Society, ACM Press, St. Louis, Missouri, USA, 442--450.
[5]
Frias, M. F., Lopez Pombo, C. G., and Aguirre, N. M. 2004. An equational calculus for Alloy. In Proceedings of the Sixth International Conference on Formal Engineering Methods (ICFEM), J. Davies, W. Schulte, and M. Barnett, Eds. Lecture Notes in Computer Science, vol. 3308. Springer-Verlag, Seattle, Washington, 162--175.
[6]
Frias, M. F., Lopez Pombo, C. G., Baum, G. A., Aguirre, N., and Maibaum, T. S. E. 2005b. Reasoning about static and dynamic properties in alloy: A purely relational approach. ACM Trans. Softw. Eng. Meth. 14, 4, 478--526.
[7]
Goldberg, E. and Novikov, Y. 2002. BerkMin: A fast and robust SAT-solver. In Proceedings of the Conference on Design, Automation and, Test in Europe, C. D. Kloos and J. da Franca, Eds. IEEE Computer Society, Paris, France, 142--149.
[8]
Harel, D., Kozen, D., and Tiuryn, J. 2000. Dynamic logic. Foundations of Computing. MIT Press, Cambridge, MA.
[9]
Hoare, C. A. R. 1969. An axiomatic basis for computer programming. Comm. ACM 12, 10, 576--583.
[10]
Jackson, D. 2002a. Alloy: A lightweight object modelling notation. ACM Trans. Softw. Eng. Meth. 11, 2, 256--290.
[11]
Jackson, D. 2002b. Micromodels of Software: Lightweight Modelling and Analysis with Alloy. MIT Laboratory for Computer Science, Cambridge, MA.
[12]
Jackson, D., Shlyakhter, I., and Sridharan, M. 2001. A micromodularity mechanism. In Proceedings of the 8th European Software Engineering Conference Held Together with the 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM Press, Vienna, Austria, 62--73.
[13]
Jones, C. 1986. Systematic Software Development Using VDM. Prentice Hall, Hertfordshire, UK.
[14]
Lopez Pombo, C. G., Owre, S., and Shankar, N. 2002. A Semantic Embedding of the Ag Dynamic Logic in PVS. Tech. Rep. SRI-CSL-02-04, Computer Science Laboratory, SRI International. July.
[15]
Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., and Malik, S. 2001. Chaff: engineering an efficient SAT solver. In Proceedings of the 38th Conference on Design Automation, J. Rabaey, Ed. ACM Press, Las Vegas, Nevada, 530--535.
[16]
Object Management Group. 1997. Object Constraint Language Specification. Object Management Group, Needham, MA. version 1.1.
[17]
Owre, S., Shankar, N., Rushby, J. M., and Stringer-Calvert, D. 2001. PVS Language Reference, Version 2.4 ed. SRI International.
[18]
Spivey, J. M. 1988. Understanding Z: A Specification Language and Its Formal Semantics. Cambridge University Press, New York, NY.

Cited By

View all
  • (2023)A Study of the Electrum and DynAlloy Dynamic Behavior NotationsIEEE Transactions on Software Engineering10.1109/TSE.2023.332062549:11(4946-4963)Online publication date: 1-Nov-2023
  • (2023) A comparison of three solver-aided programming languages: Rby, ProB, and Rosette Journal of Computer Languages10.1016/j.cola.2023.10123877(101238)Online publication date: Nov-2023
  • (2019)Translating alloy and extensions to classical BScience of Computer Programming10.1016/j.scico.2019.102378(102378)Online publication date: Dec-2019
  • Show More Cited By

Recommendations

Reviews

James Dennis Kiper

Alloy is a well-known language and tool for specification or modeling of a software system in a formal way: it can be syntactically checked for static errors, and can also be analyzed for dynamic properties. One of the characteristics of Alloy is that it does not specifically represent state, thus requiring the use of traces. Frias et al. make a compelling argument for their system, called DynAlloy. This language and tool augments Alloy by supporting actions and using these in the specification of assertions about execution traces. Through a series of examples and case studies, the authors illustrate that use of actions in specification is considerably easier to understand, and the analysis of these specifications is substantially more efficient than the Alloy equivalent. They achieve this by using Alloy formulas with the weakest liberal preconditions as the translation of DynAlloy's partial-correctness assertions. The resulting Alloy formulas may be large and complex, but they are not visible to the user. The authors then describe a method of modularization of specifications called program atomization, which allows complex specifications to be analyzed efficiently. They validate that this method does not produce false positives through a formal proof. The authors admit to at least one restriction of DynAlloy over Alloy: currently, the former does not permit specification of liveness properties. On a final note, some knowledge of Alloy is helpful in understanding this paper. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Software Engineering and Methodology
ACM Transactions on Software Engineering and Methodology  Volume 17, Issue 1
December 2007
100 pages
ISSN:1049-331X
EISSN:1557-7392
DOI:10.1145/1314493
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 December 2007
Accepted: 01 January 2007
Revised: 01 July 2006
Received: 01 August 2005
Published in TOSEM Volume 17, Issue 1

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Alloy
  2. dynamic logic
  3. software specification
  4. software validation

Qualifiers

  • Research-article
  • Research
  • Refereed

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)3
  • Downloads (Last 6 weeks)0
Reflects downloads up to 13 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)A Study of the Electrum and DynAlloy Dynamic Behavior NotationsIEEE Transactions on Software Engineering10.1109/TSE.2023.332062549:11(4946-4963)Online publication date: 1-Nov-2023
  • (2023) A comparison of three solver-aided programming languages: Rby, ProB, and Rosette Journal of Computer Languages10.1016/j.cola.2023.10123877(101238)Online publication date: Nov-2023
  • (2019)Translating alloy and extensions to classical BScience of Computer Programming10.1016/j.scico.2019.102378(102378)Online publication date: Dec-2019
  • (2019)Inductive verification of data model invariants in web applications using first-order logicAutomated Software Engineering10.1007/s10515-018-0249-226:2(379-416)Online publication date: 1-Jun-2019
  • (2018)Proof assisted bounded and unbounded symbolic model checking of software and system modelsScience of Computer Programming10.1016/j.scico.2017.08.013158(41-63)Online publication date: Jun-2018
  • (2018)A Translation from Alloy to BAbstract State Machines, Alloy, B, TLA, VDM, and Z10.1007/978-3-319-91271-4_6(71-86)Online publication date: 8-May-2018
  • (2017)DynAlloy analyzer: a tool for the specification and analysis of alloy models with dynamic behaviourProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3122826(969-973)Online publication date: 21-Aug-2017
  • (2016)Finding access control bugs in web applications with CanCheckProceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering10.1145/2970276.2970350(155-166)Online publication date: 25-Aug-2016
  • (2016)Lightweight specification and analysis of dynamic systems with rich configurationsProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2950290.2950318(373-383)Online publication date: 1-Nov-2016
  • (2016)Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software EngineeringundefinedOnline publication date: 1-Nov-2016
  • Show More Cited By

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media