Paulo's Home Page

 

:. Articles and Reports


Extending Relational Algebra with the Data Mapper operator

Application scenarios such as legacy data migration, ETL processes, and data cleaning often require to transform an input tuple into several output tuples. Relational algebra is not expressive enough to specify this kind of operation. In this paper, we propose the mapper operator to address this class of data transformations as an extension to the relational algebra. Informally, this operator iterates over the tuples of the input relation, applies a set of domain-specific functions and generates one or more output tuples for each input tuple. We also supply a
set of algebraic rewriting rules for optimizing expressions that combine standard relational operators with mappers.

Execution of data mappers

Data mappers are essential operators for implementing data transformations supporting schema mapping and integration scenarios such as legacy data migration, ETL processes for data warehousing, data cleaning activities, and business integration initiatives. Despite their widespread use, no formalization of this important operation has been proposed so far. In this paper we propose the data mapper operator as an extension to the relational algebra. We supply a set of algebraic rewriting rules for optimizing queries that combine standard relational operators with data mappers. Finally, we analyze possible algorithms for their efficient physical execution.

Efficient development of data migration transformations

In this paper we present a data transformation tool named Data Fusion. We concentrate on the following main features: A domain specific language designed to conveniently model complex data transformations, an integrated development environment to assist users on managing complex data data transformation projects, and an auditing facilitythat provides relevant information to project managers and external auditors.
  • We have presented this work at ISWC'03
  • A demo paper of this tools is also accepted for SIGMOD'04

A compiler and simulator for partial recursive functions over neural networks

It was shown that Artificial Recurrent Neural Networks have the same computing power as Turing machines (cf. [Siegelman 1995], [Siegelman 1999]). A Turing machine can be programmed in a proper high-level language — the language of partial recursive functions. In this paper we present the implementation of a compiler that directly translates high-level Turing machine programs to Artificial Recursive Neural Networks. The application contains a simulator that can be used to test the resulting networks. We also argue that these experiments provide clues to develop procedures for automatic synthesis of Neural Networks from high-level descriptions.

Automatically Verifying an Object-Oriented Specification of the Steam-Boiler System

Correctness is a desired property of industrial software systems. Although the employment of formal methods and their verification techniques in embedded realtime systems has started to be a common practice, the same cannot be said about object-oriented software. This paper presents an experiment of a technique for the automated verification of a subset of the object-oriented language OBLOG. In our setting, object-oriented models are automatically translated to LOTOS specifications using a programmable rule-based engine included in the Development Environment of the OBLOG language. The resulting specifications are then verified by model-checking using the Cadp tool-box. To illustrate the concept we develop and verify an object-oriented specification of a well known case study — the Steam-Boiler Control System.
  • See the overview of our work made by INRIA
  • Get the paper directly from GMD
  • Get the original thesis presentation for staroffice... and the exported powerpoint... version

Automatic Verification of OBLOG specifications

Designing correct software has been a problem for as long as computers have existed. Although Software engineering methodologies have contributed to the increasing quality of software systems, they cannot be successful without appropriate tools. Recent advances in a branch of software engineering that borrows concepts from discrete mathematics named Formal Methods, has enabled the automatic verification of computer systems although with some limitations. The two main verification approaches that emerged from Formal Methods are called Automatic Theorem Proving and Model-Checking. These two approaches left academia and have achieved success in the verification of real world systems. An obstacle for the extended use of these tools is requiring the formalization of systems in mathematical based notations. This thesis intends to take a step further in the direction of automatic verification of software by proposing a strategy for the verification of a high-level object-oriented specification language. The approach presented here is based on a translation of a subset of OBLOG specifications into two different formalisms: The Process Algebraic language LOTOS and Communicating Automata. These concepts were tested in the verification of the Alternating Bit Protocol with acceptable results.


 

 

<< back
All Content © 2003, 2004 Paulo J. F. Carreira