skip to main content
article

Reasoning about static and dynamic properties in alloy: A purely relational approach

Published: 01 October 2005 Publication History

Abstract

We study a number of restrictions associated with the first-order relational specification language Alloy. The main shortcomings we address are:---the lack of a complete calculus for deduction in Alloy's underlying formalism, the so called relational logic,---the inappropriateness of the Alloy language for describing (and analyzing) properties regarding execution traces.The first of these points was not regarded as an important issue during the genesis of Alloy, and therefore has not been taken into account in the design of the relational logic. The second point is a consequence of the static nature of Alloy specifications, and has been partly solved by the developers of Alloy; however, their proposed solution requires a complicated and unstructured characterization of executions.We propose to overcome the first problem by translating relational logic to the equational calculus of fork algebras. Fork algebras provide a purely relational formalism close to Alloy, which possesses a complete equational deductive calculus. Regarding the second problem, we propose to extend Alloy by adding actions. These actions, unlike Alloy functions, do modify the state. Much the same as programs in dynamic logic, actions can be sequentially composed and iterated, allowing them to state properties of execution traces at an appropriate level of abstraction.Since automatic analysis is one of Alloy's main features, and this article aims to provide a deductive calculus for Alloy, we show that:---the extension hereby proposed does not sacrifice the possibility of using SAT solving techniques for automated analysis,---the complete calculus for the relational logic is straightforwardly extended to a complete calculus for the extension of Alloy.

References

[1]
Abrial, J. 1996. The B-Book: assigning programs to meanings. Cambridge University Press, New York, NY.]]
[2]
Arkoudas, K. 2000. Denotational proof languages. Ph.D. thesis, Massachusetts Institute of Technology.]]
[3]
Arkoudas, K., Khurshid, S., Marinov, D., and Rinard, M. 2004. Integrating model checking and theorem proving for relational reasoning. In Proceedings of the 7th Conference on Relational Methods in Computer Science (RelMiCS)--2nd. International Workshop on Applications of Kleene Algebra, R. Berghammer and B. Möller, Eds. Lecture Notes in Computer Science, vol. 3051. Springer-Verlag, Malente, Germany, 204--213.]]
[4]
Bickford, M. and Guaspari, D. 1998. Lightweight analysis of UML. Tech. Rep. TM-98-0036, Odyssey Research Associates, Ithaca, NY, November.]]
[5]
Booch, G., Rumbaugh, J., and Jacobson, I. 1998. The Unified Modeling Language User Guide. Addison--Wesley Longman Publishing Co., Inc., Boston, MA.]]
[6]
Burris, S. and Sankappanavar, H. P. 1981. A Course in Universal Algebra. Graduate Texts in Mathematics. Springer-Verlag, Berlin, Germany.]]
[7]
Clarke, E. M., Grumberg, O., and Peled, D. 2000. Model Checking. MIT Press, Cambridge, MA.]]
[8]
Cleaveland, R., Klein, M., and Steffen, B. 1993. Faster model checking for the modal mu-calculus. In Proceedings of Computer Aided Verification (CAV), G. von Bochmann and D. K. Probst, Eds. Lecture Notes in Computer Science, vol. 663. Springer-Verlag, Montreal, Canada, 410--422.]]
[9]
Dijkstra, E. W. and Scholten, C. S. 1990. Predicate Calculus and Program Semantics. Springer-Verlag, New York, NY.]]
[10]
Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, C., Parent, C., Paulin-Mohring, C., and Werner, B. 1993. The coq proof assistant user's guide (version 5.8). Tech. Rep. 154, INRIA, Rocquencourt, France.]]
[11]
Frias, M. F. 2002. Fork Algebras in Algebra, Logic and Computer Science. Advances in Logic, vol. 2. World Scientific Publishing Co., Singapore.]]
[12]
Frias, M. F., Baum, G. A., and Maibaum, T. S. E. 2002. Interpretability of first-order dynamic logic in a relational calculus. In Proceedings of the 6th. Conference on Relational Methods in Computer Science (RelMiCS)---TARSKI, H. de Swart, Ed. Lecture Notes in Computer Science, vol. 2561. Springer-Verlag, Oisterwijk, The Netherlands, 66--80.]]
[13]
Frias, M. F., Haeberer, A. M., and Veloso, P. A. S. 1997. A finite axiomatization for fork algebras. Logic Journal of the IGPL 5, 3, 311--319.]]
[14]
Frias, M. F., Lopez Pombo, C. G., Baum, G. A., Aguirre, N. M., and Maibaum, T. S. E. 2003. Taking Alloy to the movies. In Proceedings of FM 2003: the 12th International FME Symposium, K. Araki, S. Gnesi, and D. Mandrioli, Eds. Lecture Notes in Computer Science, vol. 2805. Springer-Verlag, Pisa, Italy, 678--697.]]
[15]
Gordon, M. J. and Melham, T. F., Eds. 1993. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York, NY.]]
[16]
Harel, D., Kozen, D., and Tiuryn, J. 2000. Dynamic Logic. Foundations of Computing. MIT Press, Cambridge, MA.]]
[17]
Jackson, D. 2000. Automating first-order relational logic. In Proceedings of the 8th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM Press, San Diego, California, 130--139.]]
[18]
Jackson, D. 2002a. Alloy: a lightweight object modelling notation. ACM Trans. Soft. Eng. Meth. 11, 2, 256--290.]]
[19]
Jackson, D. 2002b. A Micromodel of Software: Lightweight Modelling and Analysis with Alloy. MIT Laboratory for Computer Science, Cambridge, MA.]]
[20]
Jackson, D., Schechter, I., and Shlyahter, H. 2000. Alcoa: the alloy constraint analyzer. In Proceedings of the 22nd. International Conference on Software Engineering, C. Ghezzi, M. Jazayeri, and A. L. Wolf, Eds. Association for the Computer Machinery and IEEE Computer Society, ACM Press, Limerick, Ireland, 730--733.]]
[21]
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.]]
[22]
Jackson, D. and Sullivan, K. 2000. COM revisited: tool-assisted modelling of an architectural framework. In Proceedings of the 8th ACM SIGSOFT International Symposium on Foundations of Software Engineering: Twenty-First Century Applications, D. S. Rosenblum, Ed. ACM Press, San Diego, CA, 149--158.]]
[23]
Jones, C. 1986. Systematic Software Development Using VDM. Prentice Hall, Hertfordshire, UK.]]
[24]
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.]]
[25]
Manna, Z., Anuchitanukul, A., Bj⊘rner, N., Browne, A., Chang, E., Colon, M., de Alfaro, L., Devarajan, H., Sipma, H., and Uribe, T. 1994. STeP: The stanford temporal prover. Tech. Rep., Stanford University, Stanford, CA.]]
[26]
McMillan, K. L. 1993. Symbolic Model Checking. Kluwer Academic Publishers, Norwell, MA.]]
[27]
Nipkow, T., Paulson, L. C., and Wenzel, M. 2002. Isabelle/HOL---A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer-Verlag, Berlin, Germany.]]
[28]
Object Management Group. 1997. Object Constraint Language Specification. Object Management Group, Needham, MA, version 1.1.]]
[29]
Owre, S., Rushby, J. M., and Shankar, N. 1992. PVS: A prototype verification system. In Proceedings of the 11th International Conference on Automated Deduction (CADE), D. Kapur, Ed. Lecture Notes in Artificial Intelligence, vol. 607. Springer-Verlag, Saratoga, NY, 148--752.]]
[30]
Owre, S., Rushby, J. M., Shankar, N., and Stringer-Calvert, D. 1998. PVS: an experience report. In Proceedings of Applied Formal Methods -- (FM-Trends) '98, D. Hutter, W. Stephan, P. Traverso, and M. Ullman, Eds. Lecture Notes in Computer Science, vol. 1641. Springer-Verlag, Boppard, Germany, 338--345.]]
[31]
Owre, S. and Shankar, N. 1993. Abstract datatypes in PVS. Tech. Rep. SRI-CSL-93-9R, Computer Science Laboratory, SRI International. December. Subtantially revised in June 1997.]]
[32]
Owre, S., Shankar, N., Rushby, J. M., and Stringer-Calvert, D. 2001a. PVS Language Reference, Version 2.4 ed. SRI International.]]
[33]
Owre, S., Shankar, N., Rushby, J. M., and Stringer-Calvert, D. 2001b. PVS Prover Guide, Version 2.4 ed. Computer Science Laboratory, SRI International.]]
[34]
Owre, S., Shankar, N., Rushby, J. M., and Stringer-Calvert, D. 2001c. PVS System Guide, Version 2.4 ed. Computer Science Laboratory, SRI International.]]
[35]
Spivey, J. M. 1988. Understanding Z: A Specification Language and its Formal Semantics. Cambridge University Press, New York, NY.]]
[36]
Tarski, A. and Givant, S. 1987. A Formalization of Set Theory Without Variables. American Mathematical Society Colloqium Publications, Providence, RI.]]
[37]
Vardi, M. Y. and Wolper, P. 1986. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings of the Symposium on Logic in Computer Science '86, A. Meyer, Ed. IEEE Computer Society, Cambridge, MA, 332--344.]]

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
  • (2022)Dash: declarative behavioural modelling in Alloy with control state hierarchySoftware and Systems Modeling (SoSyM)10.1007/s10270-022-01012-122:2(733-749)Online publication date: 6-Aug-2022
  • (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
  • Show More Cited By

Recommendations

Reviews

Rosziati Ibrahim

Alloy is a first-order relational specification language that originates from the Z formal specification language, which is based on mathematical models and notations. Alloy is defined using a relational logic (RL), a logic with a clear semantics based on relations and a counter-example extraction mechanism for its analysis technique. In this context, the tool is used to search for counter-examples of specifications for the purpose of validation. The advantage of Alloy is its ability to automate the process for the analysis of specifications. However, Alloy still has room for improvement. In this paper, the authors introduce two new features of the Alloy language. First, they introduce the fork relational logic (FRL) as the equational calculus of fork algebras in Alloy. This is used to deal with deduction in the language. Second, the authors extend the language to incorporate actions that enhance the FRL's expressiveness with dynamic logic features. The authors took a very systematic approach in their paper, providing a solid overview of Alloy. They begin by introducing the Alloy specification language using a simple example: specifying systems involving memories with cache. They then summarize the features and deficiencies of Alloy, and introduce the two new features (mentioned above). In formal specification languages, symbols and notations are used to analyze and design software. The symbols and notations used in this paper require readers to be familiar with Alloy specifications. This paper is recommended for readers who are interested in the Alloy language. 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 14, Issue 4
October 2005
146 pages
ISSN:1049-331X
EISSN:1557-7392
DOI:10.1145/1101815
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: 01 October 2005
Published in TOSEM Volume 14, Issue 4

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Alloy
  2. fork algebras
  3. relational specifications

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)8
  • 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
  • (2022)Dash: declarative behavioural modelling in Alloy with control state hierarchySoftware and Systems Modeling (SoSyM)10.1007/s10270-022-01012-122:2(733-749)Online publication date: 6-Aug-2022
  • (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
  • (2010)Programming with angelic nondeterminismACM SIGPLAN Notices10.1145/1707801.170633945:1(339-352)Online publication date: 17-Jan-2010
  • (2010)Programming with angelic nondeterminismProceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1706299.1706339(339-352)Online publication date: 17-Jan-2010
  • (2009)A Complete Set of Object Modeling Laws for AlloyFormal Methods: Foundations and Applications10.1007/978-3-642-10452-7_14(204-219)Online publication date: 5-Nov-2009
  • (2008)AlchemyProceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering10.1145/1453101.1453123(158-169)Online publication date: 9-Nov-2008
  • (2008)Towards Abstraction for DynAlloy SpecificationsProceedings of the 10th International Conference on Formal Methods and Software Engineering10.1007/978-3-540-88194-0_14(207-225)Online publication date: 27-Oct-2008
  • (2007)Model checking with SAT-based characterization of ACTL formulasProceedings of the formal engineering methods 9th international conference on Formal methods and software engineering10.5555/1775348.1775365(191-211)Online publication date: 14-Nov-2007
  • (2007)Efficient Analysis of DynAlloy SpecificationsACM Transactions on Software Engineering and Methodology10.1145/1314493.131449717:1(1-34)Online publication date: 12-Dec-2007
  • 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