Skip to main content
SpringerLink
Log in
Book cover

International Conference on Abstract State Machines, Alloy, B and Z

ABZ 2010: Abstract State Machines, Alloy, B and Z pp 363–376Cite as

Towards Formally Templated Relational Database Representations in Z

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5977))

Abstract

Many authors have drawn parallels between the relational model of data and the formal description technique Z, yet none of these contributions have managed to be both close to the relational model in terms of providing a practical means of database design and fully formal in terms of providing an appropriate metamodel. We compare these various formalisms, and suggest how the use of the formal template approach of Amálio et al might help to overcome some of the issues faced. We demonstrate the application of this work via a short case study, and suggest further enhancements to the template language.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Codd, E.F.: A relational model of data for large shared data banks. Communications of the ACM 13(6), 377–387 (1970)

    Article  MATH  Google Scholar 

  2. Spivey, J.M.: The Z notation: A Reference Manual. Prentice-Hall, Englewood Cliffs (1992)

    Google Scholar 

  3. van Diepen, M.J., van Hee, K.M.: A Formal Semantics for Z and the Link between Z and the Relational Algebra. In: Langmaack, H., Hoare, C.A.R., Bjorner, D. (eds.) VDM 1990. LNCS, vol. 428, pp. 526–551. Springer, Heidelberg (1990)

    Google Scholar 

  4. Edmond, D.: Information Modeling: Specification and Implementation. Prentice-Hall, Englewood Cliffs (1992)

    Google Scholar 

  5. Davies, J.W.M., Simpson, A.C., Martin, A.P.: Teaching Formal Methods in Context. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 185–202. Springer, Heidelberg (2004)

    Google Scholar 

  6. Schewe, K.D., Schmidt, J.W., Wetzel, I.: Specification and refinement in an integrated database application environment. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 551, pp. 496–510. Springer, Heidelberg (1991)

    Google Scholar 

  7. Hayes, I.: VDM and Z: A comparative case study. Formal Aspects of Computing 4(1), 76–99 (1992)

    Article  MATH  Google Scholar 

  8. Mammar, A., Laleau, R.: Design of an automatic prover dedicated to the refinement of database applications. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 834–854. Springer, Heidelberg (2003)

    Google Scholar 

  9. Mammar, A., Laleau, R.: A formal approach based on UML and B for the specification and development of database applications. Automated Software Engineering 13(4), 497–528 (2006)

    Article  Google Scholar 

  10. Laleau, R., Polack, F.: Specification of integrity-preserving operations in information systems by using a formal UML-based language. Information & Software Technology 43(12), 693–704 (2001)

    Article  Google Scholar 

  11. Laleau, R., Polack, F.: Using formal metamodels to check consistency of functional views in information systems specification. Information & Software Technology 50(7-8), 797–814 (2008)

    Article  Google Scholar 

  12. Davies, J.W.M., Welch, J., Cavarra, A.L., Crichton, E.: On the Generation of Object Databases using Booster. In: Proceedings of the 11th IEEE Conference on the Engineering of Complex Computer Systems (2006)

    Google Scholar 

  13. Gray, D.: The Formal Specification of a Small Bookshop Information System. IEEE Transactions on Software Engineering 14(2), 263–272 (1988)

    Article  Google Scholar 

  14. Amálio, N., Stepney, S., Polack, F.: Formal Proof from UML Models. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 418–433. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  15. Sufrin, B.A., Morgan, C.C., Sørensen, I.H., Hayes, I.J.: Notes for a Z handbook. Programming Research Group, Oxford University Computing Laboratory (1984)

    Google Scholar 

  16. Hayes, I.J., Jones, C.B., Nicholls, J.E.: Understanding the differences between VDM and Z. ACM SIGSOFT Software Engineering Notes 19(3), 75–81 (1994)

    Article  Google Scholar 

  17. Edmond, D.: Refining Database Systems. In: Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1995. LNCS, vol. 967, pp. 25–44. Springer, Heidelberg (1995)

    Google Scholar 

  18. de Barros, R.S.M.: Deriving Relational Database Programs from Formal Specifications. In: Naftalin, M., Bertrán, M., Denvir, T. (eds.) FME 1994. LNCS, vol. 873, p. 703. Springer, Heidelberg (1994)

    Google Scholar 

  19. de Barros, R.S.M.: On the Formal Specification and Derivation of Relational Database Applications. PhD thesis, Dept. of Computing Science, University of Glasgow (1994)

    Google Scholar 

  20. Martin, A.P., Simpson, A.C.: Generalising the Z schema calculus: database schemas and beyond. In: Proceedings of APSEC 2003, pp. 28–37 (2003)

    Google Scholar 

  21. Amálio, N., Stepney, S., Polack, F.: A Formal Template Language Enabling Metaproof. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 252–267. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  22. Hall, A.: Specifying and Interpreting Class Hierarchies in Z. In: Proceedings of the 1994 Z User Workshop, pp. 120–138 (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK

    Nicolas Wu & Andrew Simpson

Authors
  1. Nicolas Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrew Simpson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Département d’informatique, Sherbrooke, Université de Sherbrooke, J1K 2R1, Québec, Canada

    Marc Frappier

  2. School of Computing Science, Simon Fraser University, V5A 1S6, Burnaby, BC, Canada

    Uwe Glässer

  3. Department of Electrical and computer Engineering, University of Texas at Austin, 1 University Station C5000, 78712-0240, Austin, TX, USA

    Sarfraz Khurshid

  4. Département informatique, Route forestiére Hurtault, Université Paris-Est Créteil, IUT Sénart/Fontainebleau, 77300, Fontainebelau, France

    Régine Laleau

  5. Department of Computer Science, The University of Waikato, 3240, Hamilton, New Zealand

    Steve Reeves

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wu, N., Simpson, A. (2010). Towards Formally Templated Relational Database Representations in Z. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds) Abstract State Machines, Alloy, B and Z. ABZ 2010. Lecture Notes in Computer Science, vol 5977. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11811-1_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11811-1_27

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11810-4

  • Online ISBN: 978-3-642-11811-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation