Recent Publications

Coelho F, Pereira JO, Vilaça R, Oliveira R.  2016.  Holistic Shuffler for the Parallel Processing of SQL Window Functions. Distributed Applications and Interoperable Systems - 16th {IFIP} {WG} 6.1 International Conference, {DAIS} 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June. :75–81. Abstractholistic-proceedings.pdf

Window functions are a sub-class of analytical operators that allow data to be handled in a derived view of a given relation, while taking into account their neighboring tuples. Currently, systems bypass parallelization opportunities which become especially relevant when considering Big Data as data is naturally partitioned.
We present a shuffling technique to improve the parallel execution of window functions when data is naturally partitioned when the query holds a partitioning clause that does not match the natural partitioning of the relation. We evaluated this technique with a non-cumulative ranking function and we were able to reduce data transfer among parallel workers in 85% when compared to a naive approach.

Coelho F, Pereira JO, Vilaça R, Oliveira R.  2016.  Reducing Data Transfer in Parallel Processing of SQL Window Functions. Proceedings of the 6th International Conference on Cloud Computing and Services Science. :343-347. Abstractdatadiversityconvergence_2016_1_copy.pdf

Window functions are a sub-class of analytical operators that allow data to be handled in a derived view of a given relation, while taking into account their neighboring tuples. We propose a technique that can be used in the parallel execution of this operator when data is naturally partitioned. The proposed method benefits the cases where the required partitioning is not the natural partitioning employed. Preliminary evaluation shows that we are able to limit data transfer among parallel workers to 14\% of the registered transfer when using a naive approach.

Maia F, Matos M, Coelho F.  2016.  Towards Quantifiable Eventual Consistency. Proceedings of the 6th International Conference on Cloud Computing and Services Science. :368-370. Abstractdatadiversityconvergence_2016_5.pdf

In the pursuit of highly available systems, storage systems began offering eventually consistent data models. These models are suitable for a number of applications but not applicable for all. In this paper we discuss a system that can offer a eventually consistent data model but can also, when needed, offer a strong consistent one.

Lourenço CB, Frade MJ, Pinto JS.  2016.  Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach. Programming Languages and Systems - 25th European Symposium on Programming, {ESOP} 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 9632:41–67. Abstractesop2016.pdf

Deductive verification tools typically rely on the conversion of code to a single-assignment (SA) form. In this paper we formalize pro- gram verification based on the translation of While programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct, and the subsequent generation of compact, indeed linear-size, verification conditions. Soundness and completeness proofs are given for the entire workflow, including the translation of an- notated programs to SA form. The formalization is based on a program logic that we show to be adaptation-complete. Although this important property has not, as far as we know, been established for any existing program verification tool, we believe that adaptation-completeness is one of the major motivations for the use of SA form as an intermediate lan- guage. Our results here show that indeed this allows for the tools to achieve the maximum degree of adaptation when handling subprograms.

Ramos MVM, de Queiroz RJGB, Moreira N, Almeida JB.  2016.  On the Formalization of Some Results of Context-Free Language Theory. Logic, Language, Information, and Computation – 23rd International Workshop, WoLLIC 2016. 9803 Abstract16wollic.pdf

This work describes a formalization effort, using the Coq proof assistant, of fundamental results related to the classical theory of context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimi- nation of useless symbols, inaccessible symbols, empty rules and unit rules), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the important result that is the formalization of the Pumping Lemma for context-free languages.

Cledou MG, Barbosa LS.  2016.  An Ontology for Licensing Public Transport Services. Proceedings of the 9th International Conference on Theory and Practice of Electronic Governance. :230–239. Abstractan_ontology_for_licensing_public_transport_services.pdf

By 2050 it is expected that 66% of the world population will reside in cities, compared to 54% in 2014. One particular challenge associated to urban population growth refers to transportation systems, and as an approach to face it, governments are investing significant efforts enhancing public transport services. An important aspect of public transport is ensuring that licensing of such services fulfill existing government regulations. Due to the differences in government regulations, and to the difficulties in ensuring the fulfillment of their specific features, many local governments develop tailored Information and Communication Technology (ICT) solutions to automate the licensing of public transport services. In this paper we propose an ontology for licensing such services following the REFSENO methodology. In particular, the ontology captures common concepts involved in the application and processing stage of licensing public bus passenger services. The main contribution of the proposed ontology is to define a common vocabulary to share knowledge between domain experts and software engineers, and to support the definition of a software product line for families of public transport licensing services.

Gonçalves RC, Pereira JO, Jimenez-Peris R.  2016.  An RDMA Middleware for Asynchronous Multi-stage Shuffling in Analytical Processing. DAIS '16: Proceedings of the 16th IFIP International Conference on Distributed Applications and Interoperable Systems. Abstract

A key component in large scale distributed analytical processing is shuffling, the distribution of data to multiple nodes such that the computation can be done in parallel. In this paper we describe the design and implementation of a communication middleware to support data shuffling for executing multi-stage analytical processing operations in parallel. The middleware relies on RDMA (Remote Direct Memory Access) to provide basic operations to asynchronously exchange data among multiple machines. Experimental results show that the RDMA-based middleware developed can provide a 75 % reduction of the costs of communication operations on parallel analytical processing tasks, when compared with a sockets middleware.

Cruz F, Maia F, Matos M, Oliveira R, Paulo J, Pereira JO, Vilaça R.  2016.  Resource Usage Prediction in Distributed Key-Value Datastores. Distributed Applications and Interoperable Systems: 16th IFIP WG 6.1 International Conference, DAIS 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2. :144–159. Abstract

n/a

Rani S, Koshley DK, Halder R.  2016.  A Watermarking Framework for Outsourced and Distributed Relational Databases. In Proceedings of the 3rd International Conference on Future Data and Security Engineering (FDSE 2016). Springer LNCS 10018 Abstract19.pdf

Unlike centralized databases, watermarking of distributed databases faces serious challenges for various reasons, e.g. (i) Distribution of data (ii) Existence of replication (iii) Preservation of watermarks while partitioning and distributing databases, etc. In this paper, we propose a novel watermarking technique for distributed relational databases considering a generic scenario that supports database outsourcing and hybrid partitioning. Our approach addresses the above challenges in an effective way by maintaining metadata and by making the detection phase partition independent. To the best of our knowledge, this is the first proposal on watermarking of distributed relational databases that supports database outsourcing and its partitioning and distribution in a distributed setting.

Jana A, Halder R.  2016.  Defining Abstract Semantics for Static Dependence Analysis of Relational Database Applications. In Proceedings of the 12th International Conference on Information Systems Security (ICISS 2016). Springer LNCS Abstract18.pdf

Dependence Graph provides the basis for powerful programming tools to address a large number of software engineering activities including security analysis. This paper proposes a semantics-based static dependence analysis framework for relational database applications based on the Abstract Interpretation theory. As database attributes di ffer from traditional imperative language variables, we define abstract semantics of database applications in relational abstract domain. This allows to identify statically various parts of database information (in abstract form) possibly used or defined by database statements, leading to a more precise dependence analysis. This way the semantics-based dependence computation improves w.r.t. its syntax-based counterpart. We prove the soundness of our proposed approach which guarantees that non-overlapping of the defined-part by one statement and the used-part by another statement in abstract domain always indicates a non-dependency in practice. Furthermore the abstract semantics as a basis of the proposed framework makes it more powerful to solve undecidable scenario when initial database state is completely unknown.

Shoker A.  2016.  Exploiting Universal Redundancy. The 15th IEEE International Symposium on Network Computing and Applications. Abstractartira.pdf

Fault tolerance is essential for building reliable services; however, it comes at the price of redundancy, mainly the “replication factor” and “diversity”. With the increasing reliance on Internet-based services, more machines (mainly servers) are needed to scale out, multiplied with the extra expense of replication. This paper revisits the very fundamentals of fault tolerance and presents “artificial redundancy”: a formal generalization of “exact copy” redundancy in which new sources of redundancy are exploited to build fault tolerant systems. On this concept, we show how to build “artificial replication” and design “artificial fault tolerance” (AFT). We discuss the properties of these new techniques showing that AFT extends current fault tolerant approaches to use other forms of redundancy aiming at reduced cost and high diversity.

Santos A, Cunha A, Macedo N, Lourenço CB.  2016.  A Framework for Quality Assessment of ROS Repositories. Abstractros_quality.pdf

Robots are being increasingly used in safety-critical contexts, such as transportation and health. The need for flexible behavior in these contexts, due to human interaction factors or unstructured operating environments, led to a transition from hardware- to software-based safety mechanisms in robotic systems, whose reliability and quality is imperative to guarantee. Source code static analysis is a key component in formal software verification. It consists on inspecting code, often using automated tools, to determine a set of relevant properties that are known to influence the occurrence of defects in the final product. This paper presents HAROS, a generic, plug-in-driven, framework to evaluate code quality, through static analysis, in the context of the Robot Operating System (ROS), one of the most widely used robotic middleware. This tool (equipped with plug-ins for computing metrics and conformance to coding standards) was applied to several publicly available ROS repositories, whose results are also reported in the paper, thus providing a first overview of the internal quality of the software being developed in this community.

Fayollas C, Martinie C, Palanque P, Masci P, Harrison MD, Campos JC, Silva SR.  2016.  Evaluation of formal IDEs for human-machine interface design and analysis: the case of CIRCUS and PVSio-web. Workshop on Integrated Formal Development Environment (F-IDE 2016), co-located with FM2016. f-ide2016-camera-ready.pdf
Costa CM, Leite CRM, Sousa AL.  2016.  Efficient SQL adaptive query processing in cloud databases systems. 2016 {IEEE} Conference on Evolving and Adaptive Intelligent Systems, {EAIS} 2016, Natal, Brazil, May 23-25, 2016. :114–121. Abstract16.pdf

n/a