Networking is becoming an intrinsic part of computation bringing with it a host of new theoretical and practical challenges. Services are hosted in virtual environments where the services outlive the computers where they are hosted: virtual computers where these services temporarily reside go up and down and migrate around different computers. This has increased the complexity of managing services and the physical networks and clusters of servers that host them. Researchers and industry have been looking for new management ideas and are playing with new models like Named Data Networking (NDN) where network addresses are replaced with data names instead of using device locations, or Software Defined Networking (SDN), where the control plane of the network (building routing tables) is removed from the network switches and routers and is implemented in software in regular computer servers

It has been recently shown that declarative database query languages, such as Datalog, could naturally be used to specify and implement network services and protocols. The approach, referred to as declarative networking, makes the specifications of complex network protocols concise and intuitive, and directly executable through distributed query processing algorithms. Applications for declarative networking go far beyond network protocols, and languages and techniques developed in this setting provide the basis for declarative distributed computing. This paradigm has been used for security and provenance in distributed query processing, in the analysis of asynchronous event systems.

There are several variants of concrete languages for specifying DDSs, but their common denominator is data­ centricity: computations in a single node are limited to evaluations of queries on a relational database (DB), and messages passed between nodes are snippets of DBs, providing a close correspondence between the programs and a formal specification in logic of their computation. Our aim in this project to provide a formal, systematic characterization of verification of DDSs.

This work complements a project in which one of the PI has been involved in collaboration with IBM T. J. Watson Research Center and the Department of Computing at Imperial College London that has been developing a system (depicted in the figure below) for the analysis and execution of declaratively specified distributed programs. Details of the system can be found  here. The results of the project will help to guide the development of new verification tools.

To know more:

• Presentation by Jorge Lobo at the Data-driven Knowledge Extraction Workshop, June 2016, Barcelona

Slides and work referenced: J. Ma, F. Le, A. Russo and J. Lobo, "Declarative Framework for Specification, Simulation and Analysis of Distributed Applications," in IEEE Transactions on Knowledge and Data Engineering, vol. 28, no. 6, pp. 1489-1502.