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

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: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 2: Konstantinos Arkoudas , Olin Shivers, Denotational proof languages, 2000
• 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: Grady Booch , James Rumbaugh , Ivar Jacobson, The Unified Modeling Language user guide, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1999
• 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: Rance Cleaveland , Marion Klein , Bernhard Steffen, Faster Model Checking for the Modal Mu-Calculus, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.410-422, June 29-July 01, 1992
• 9: Edsger W. Dijkstra , Carel S. Scholten, Predicate calculus and program semantics, Springer-Verlag New York, Inc., New York, NY, 1990
• 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: M. Frias , Marcelo Fabian Frias, Fork Algebras in Algebra, Logic and Computer Science, World Scientific Publishing Co., Inc., River Edge, NJ, 2002
• 12: Marcelo F. Frias , Gabriel Baum , T. S. E. Maibaum, Interpretability of First-Order Dynamic Logic in a Relational Calculus, Revised Papers from the 6th International Conference and 1st Workshop of COST Action 274 TARSKI on Relational Methods in Computer Science, p.66-80, October 16-21, 2001
• 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: M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
• 16: David Harel , Jerzy Tiuryn , Dexter Kozen, Dynamic Logic, MIT Press, Cambridge, MA, 2000
• 17: Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
• 18: Daniel Jackson, Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.2, p.256-290, April 2002 [doi>10.1145/505145.505149]
• 19: Jackson, D. 2002b. A Micromodel of Software: Lightweight Modelling and Analysis with Alloy. MIT Laboratory for Computer Science, Cambridge, MA.
• 20: Daniel Jackson , Ian Schechter , Hya Shlyahter, Alcoa: the alloy constraint analyzer, Proceedings of the 22nd international conference on Software engineering, p.730-733, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337616]
• 21: Daniel Jackson , Ilya Shlyakhter , Manu Sridharan, A micromodularity mechanism, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 22: Daniel Jackson , Kevin Sullivan, COM revisited: tool-assisted modelling of an architectural framework, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.149-158, November 06-10, 2000, San Diego, California, United States
• 23: C B Jones, Systematic software development using VDM, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1986
• 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: Z Manna , Anuchit Anuchitanukul , Nikolaj Bjorner , Anca Browne , Edward Chang , Michael Colon , Luca de Alfaro , Harish Devarajan , Henny Sipma , Tomas Uribe, STeP: The Stanford Temporal Prover, Stanford University, Stanford, CA, 1994
• 26: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 27: Isabelle/HOL: a proof assistant for higher-order logic, Springer-Verlag, London, 2002
• 28: Object Management Group. 1997. Object Constraint Language Specification. Object Management Group, Needham, MA, version 1.1.
• 29: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 30: Sam Owre , John M. Rushby , Natarajan Shankar , David W. J. Stringer-Calvert, PVS: An Experience Report, Proceedings of the International Workshop on Current Trends in Applied Formal Method: Applied Formal Methods, p.338-345, October 07-09, 1998
• 31: Owre Sam , Shankar Natarajan, Abstract Datatypes in PVS, NASA Langley Technical Report Server, 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: J. M. Spivey, Understanding Z: a specification language and its formal semantics, Cambridge University Press, New York, NY, 1988
• 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.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Keywords:
Alloy, fork algebras, relational specifications