skip to main content
10.1145/1062455.1062535acmconferencesArticle/Chapter ViewAbstractPublication PagesicseConference Proceedingsconference-collections
Article

DynAlloy: upgrading alloy with actions

Published: 15 May 2005 Publication History

Abstract

We present DynAlloy, an extension to the Alloy specification language to describe dynamic properties of systems using actions. Actions allow us to appropriately specify dynamic properties, particularly, properties regarding execution traces, in the style of dynamic logic specifications.We extend Alloy's syntax with a notation for partial correctness assertions, whose semantics relies on an adaptation of Dijkstra's weakest liberal precondition. These assertions, defined in terms of actions, allow us to easily express properties regarding executions, favoring the separation of concerns between the static and dynamic aspects of a system specification.We also extend the Alloy tool in such a way that DynAlloy specifications are also automatically analyzable, as standard Alloy specifications. We present the foundations, two case-studies, and empirical results evidencing that the analysis of DynAlloy specifications can be performed efficiently.

References

[1]
E. W. Dijkstra and C. S. Scholten. Predicate calculus and program semantics. Springer-Verlag, 1990.
[2]
E. Goldberg and Y. Novikov. BerkMin: A fast and robust sat-solver. In Proceedings of the conference on Design, automation and test in Europe, pages 142--149. IEEE Computer Society, 2002.
[3]
D. Harel, D. Kozen, and J. Tiuryn. Dynamic logic. Foundations of Computing. MIT Press, 2000.
[4]
D. Jackson. Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology, 2002.
[5]
D. Jackson. A micromodels of software: Lightweight modelling and analysis with Alloy. MIT Laboratory for Computer Science, Cambridge, MA, 2002.
[6]
D. Jackson, I. Shlyakhter, and M. Sridharan. 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, pages 62--73, Vienna, Austria, 2001. Association for the Computer Machinery, ACM Press.
[7]
M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: engineering an efficient SAT solver. In J. Rabaey, editor, Proceedings of the 38th conference on Design automation, pages 530--535, Las Vegas, Nevada, United States, 2001. ACM Press.
[8]
J. M. Spivey. Understanding Z: a specification language and its formal semantics. Cambridge University Press, 1988.

Cited By

View all
  • (2024)Exploring the interaction of design variability and stochastic operational uncertainties in software-intensive systems through the lens of modelingSoftware and Systems Modeling10.1007/s10270-024-01226-5Online publication date: 11-Nov-2024
  • (2022)Pardinus: A Temporal Relational Model FinderJournal of Automated Reasoning10.1007/s10817-022-09642-266:4(861-904)Online publication date: 12-Sep-2022
  • (2022)Dash: declarative behavioural modelling in Alloy with control state hierarchySoftware and Systems Modeling10.1007/s10270-022-01012-122:2(733-749)Online publication date: 6-Aug-2022
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ICSE '05: Proceedings of the 27th international conference on Software engineering
May 2005
754 pages
ISBN:1581139632
DOI:10.1145/1062455
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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 May 2005

Permissions

Request permissions for this article.

Check for updates

Author Tags

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

Qualifiers

  • Article

Conference

ICSE05
Sponsor:

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (2024)Exploring the interaction of design variability and stochastic operational uncertainties in software-intensive systems through the lens of modelingSoftware and Systems Modeling10.1007/s10270-024-01226-5Online publication date: 11-Nov-2024
  • (2022)Pardinus: A Temporal Relational Model FinderJournal of Automated Reasoning10.1007/s10817-022-09642-266:4(861-904)Online publication date: 12-Sep-2022
  • (2022)Dash: declarative behavioural modelling in Alloy with control state hierarchySoftware and Systems Modeling10.1007/s10270-022-01012-122:2(733-749)Online publication date: 6-Aug-2022
  • (2021)Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field BoundsFundamental Approaches to Software Engineering10.1007/978-3-030-71500-7_11(218-239)Online publication date: 27-Mar-2021
  • (2020)HaiQProceedings of the 8th International Conference on Formal Methods in Software Engineering10.1145/3372020.3391562(22-33)Online publication date: 7-Oct-2020
  • (2020)SAT-based arithmetic support for alloyProceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering10.1145/3324884.3415285(1161-1163)Online publication date: 21-Dec-2020
  • (2020)Transitive-closure-based model checking (TCMC) in AlloySoftware and Systems Modeling10.1007/s10270-019-00763-8Online publication date: 3-Jan-2020
  • (2019)A Representation Theorem for Change through Composition of ActivitiesACM Transactions on Computational Logic10.1145/332912120:4(1-31)Online publication date: 26-Jul-2019
  • (2019)Extracting counterexamples from transitive-closure-based model checkingProceedings of the 11th International Workshop on Modelling in Software Engineerings10.1109/MiSE.2019.00015(47-54)Online publication date: 26-May-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
  • Show More Cited By

View Options

Login options

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