×

A coordination language for databases. (English) Zbl 1398.68124

Summary: We present a coordination language for the modeling of distributed database applications. The language, baptized Klaim-DB, borrows the concepts of localities and nets of the coordination language Klaim but re-incarnates the tuple spaces of Klaim as databases. It provides high-level abstractions and primitives for the access and manipulation of structured data, with integrity and atomicity considerations. We present the formal semantics of Klaim-DB and develop a type system that avoids potential runtime errors such as certain evaluation errors and mismatches of data format in tables, which are monitored in the semantics. The use of the language is illustrated in a scenario where the sales from different branches of a chain of department stores are aggregated from their local databases. Raising the abstraction level and encapsulating integrity checks in the language primitives have benefited the modeling task considerably.

MSC:

68P15 Database theory
68M14 Distributed systems

Software:

Klava; KLAIM; SCEL
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Jean-Raymond Abrial. Formal methods: Theory becoming practice. J. UCS, 13(5):619–628, 2007.
[2] Yehia Abd Alrahman, Rocco De Nicola, and Michele Loreti. On the power of attribute-based communication. In Elvira Albert and Ivan Lanese, editors, Formal Techniques for Distributed Objects, Compo- nents, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Herak- lion, Crete, Greece, June 6-9, 2016, Proceedings, volume 9688 of Lecture Notes in Computer Science, pages 1–18. Springer, 2016. · Zbl 1347.68022
[3] V’eronique Benzaken, ’Evelyne Contejean, and Stefania Dumbrava. A Coq formalization of the relational data model. In Programming Languages and Systems, pages 189–208. Springer, 2014. · Zbl 1405.68103
[4] Lorenzo Bettini, Rocco De Nicola, and Michele Loreti. Implementing Mobile and Distributed Applications in X-Klaim. Scalable Computing: Practice and Experience, Special Issue: Software Agent Mobility, 7(4):13–35, 2006.
[5] Lorenzo Bettini, Rocco De Nicola, and Rosario Pugliese. Klava: a Java Package for Distributed and Mobile Applications. Software - Practice and Experience, 32(14):1365–1394, 2002. · Zbl 1009.68933
[6] E. F. Codd. A relational model of data for large shared data banks. Commun. ACM, 13(6):377–387, 1970. · Zbl 0207.18003
[7] Rocco De Nicola, Gian Luigi Ferrari, and Rosario Pugliese. KLAIM: A kernel language for agents interaction and mobility. IEEE Trans. Software Eng., 1998.
[8] Rocco De Nicola, Daniele Gorla, Ren’e Rydhof Hansen, Flemming Nielson, Hanne Riis Nielson, Christian W. Probst, and Rosario Pugliese. From flow logic to static type systems for coordination languages. Sci. Comput. Program., 75(6):376–397, 2010. · Zbl 1192.68126
[9] Rocco De Nicola, Diego Latella, Alberto Lluch Lafuente, Michele Loreti, Andrea Margheri, Mieke Massink, Andrea Morichetta, Rosario Pugliese, Francesco Tiezzi, and Andrea Vandin. The SCEL language: Design, implementation, verification. In Martin Wirsing, Matthias M. H”olzl, Nora Koch, and Philip Mayer, editors, Software Engineering for Collective Autonomic Systems - The ASCENS Approach, volume 8998 of Lecture Notes in Computer Science, pages 3–71. Springer, 2015.
[10] Rocco De Nicola, Michele Loreti, Rosario Pugliese, and Francesco Tiezzi. A formal approach to autonomic systems programming: The SCEL language. TAAS, 9(2):7, 2014. · Zbl 1416.68051
[11] David Gelernter and Arthur J. Bernstein. Distributed communication via global buffer. In ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, Ottawa, CanadaAugust 18-20, 1982, pages 10–18, 1982.
[12] Martin Gogolla, editor. An Extended Entity-Relationship Model: Fundamentals and Pragmatics, chapter Formal semantics of SQL, pages 99–120. Springer Berlin Heidelberg, Berlin, Heidelberg, 1994.
[13] E. Kuhn and T. Ludwig. Vip-mdbs: A logic multidatabase system. In Proceedings of the First Interna- tional Symposium on Databases in Parallel and Distributed Systems, DPDS ’88, pages 190–201. IEEE Computer Society Press.
[14] Lu’ısa Louren\c{}co and Lu’ıs Caires. Information flow analysis for valued-indexed data security compartments. In Trustworthy Global Computing - 8th International Symposium, TGC 2013, pages 180–198, 2013. · Zbl 1348.68019
[15] Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. Toward a verified relational database management system. In ACM Sigplan Notices, volume 45, pages 237–248. ACM, 2010. · Zbl 1312.68083
[16] M. Negri, G. Pelagatti, and L. Sbattella. Formal semantics of sql queries. ACM Trans. Database Syst., 16(3):513–534, September 1991.
[17] Chris Newcombe. Why amazon chose tla+. In Yamine Ait Ameur and Klaus-Dieter Schewe, editors, Abstract State Machines, Alloy, B, TLA, VDM, and Z, volume 8477 of Lecture Notes in Computer Science, pages 25–39. 2014.
[18] Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. · Zbl 0995.68018
[19] Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebr. Program., 60-61:17– 139, 2004. · Zbl 1082.68062
[20] Madhan M Thirukonda and Ronaldo Menezes. On the use of Linda as a framework for distributed database systems. Technical report, 2002.
[21] Terkel K. Tolstrup, Flemming Nielson, and Ren’e Rydhof Hansen. Locality-based security policies. In Formal Aspects in Security and Trust, Fourth International Workshop, FAST 2006, pages 185–201, 2006.
[22] Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John S. Fitzgerald. Formal methods: Practice and experience. ACM Comput. Surv., 41(4), 2009.
[23] Xi Wu, Ximeng Li, Alberto Lluch Lafuente, Flemming Nielson, and Hanne Riis Nielson. Klaim-db: A modeling language for distributed database applications. In Coordination Models and Languages - 17th IFIP WG 6.1 International Conference, COORDINATION 2015, pages 197–212, 2015. · Zbl 1398.68124
[24] Mosh’e M. Zloof. Query by example. In Proceedings of the May 19-22, 1975, National Computer Con- ference and Exposition, AFIPS ’75, pages 431–438, 1975.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.