View selection for designing the global data warehouse

A global data warehouse (DW) integrates data from multiple distributed heterogeneous databases and other information sources. A global DW can be abstractly seen as a set of materialized views. The selection of views for materialization in a DW is an important decision in the design of a DW. Current commercial products do not provide tools for automatic DW design. We provide a general method that, given a set of select-project-join queries to be satisfied by the DW, generates sets of materialized views that satisfy all the input queries. This process is complex since ‘common subexpressions' between the queries need to be detected and exploited. Our method is then applied to solve the problem of selecting such a materialized view set that fits in the space allocated to the DW for materialization and minimizes the combined overall query evaluation and view maintenance cost. We design algorithms which are implemented and we report on their experimental evaluation.     

MiniCon: A scalable algorithm for answering queries using views

The problem of answering queries using views is to find efficient methods of answering a query using a set of previously materialized views over the database, rather than accessing the database relations. The problem has received significant attention because of its relevance to a wide variety of data management problems, such as data integration, query optimization, and the maintenance of physical data independence. To date, the performance of proposed algorithms has received very little attention, and in particular, their scale up in the presence of a large number of views is unknown. We first analyze two previous algorithms, the bucket algorithm and the inverse-rules, and show their deficiencies. We then describe the MiniCon, a novel algorithm for finding the maximally-contained rewriting of a conjunctive query using a set of conjunctive views. We present the first experimental study of algorithms for answering queries using views. The study shows that the MiniCon scales up well and significantly outperforms the previous algorithms. We describe an extension of the MiniCon to handle comparison predicates, and show its performance experimentally. Finally, we describe how the MiniCon can be extended to the context of query optimization. Received: 15 October 2000 / Accepted: 15 April 2001 Published online: 28 June 2001     

Answering queries using views: A survey

The problem of answering queries using views is to find efficient methods of answering a query using a set of previously defined materialized views over the database, rather than accessing the database relations. The problem has recently received significant attention because of its relevance to a wide variety of data management problems. In query optimization, finding a rewriting of a query using a set of materialized views can yield a more efficient query execution plan. To support the separation of the logical and physical views of data, a storage schema can be described using views over the logical schema. As a result, finding a query execution plan that accesses the storage amounts to solving the problem of answering queries using views. Finally, the problem arises in data integration systems, where data sources can be described as precomputed views over a mediated schema. This article surveys the state of the art on the problem of answering queries using views, and synthesizes the disparate works into a coherent framework. We describe the different applications of the problem, the algorithms proposed to solve it and the relevant theoretical results. Received: 1 August 1999 / Accepted: 23 March 2001 Published online: 6 September 2001     

The GMAP: a versatile tool for physical data independence

Physical data independence is touted as a central feature of modern database systems. It allows users to frame queries in terms of the logical structure of the data, letting a query processor automatically translate them into optimal plans that access physical storage structures. Both relational and object-oriented systems, however, force users to frame their queries in terms of a logical schema that is directly tied to physical structures. We present an approach that eliminates this dependence. All storage structures are defined in a declarative language based on relational algebra as functions of a logical schema. We present an algorithm, integrated with a conventional query optimizer, that translates queries over this logical schema into plans that access the storage structures. We also show how to compile update requests into plans that update all relevant storage structures consistently and optimally. Finally, we report on experiments with a prototype implementation of our approach that demonstrate how it allows storage structures to be tuned to the expected or observed workload to achieve significantly better performance than is possible with conventional techniques. Edited by Matthias Jarke, Jorge Bocca, Carlo Zaniolo. Received September 15, 1994 / Accepted September 1, 1995     

Monotonic complements for independent data warehouses

Views over databases have regained attention in the context of data warehouses, which are seen as materialized views. In this setting, efficient view maintenance is an important issue, for which the notion of self-maintainability has been identified as desirable. In this paper, we extend the concept of self-maintainability to (query and update) independence within a formal framework, where independence with respect to arbitrary given sets of queries and updates over the sources can be guaranteed. To this end we establish an intuitively appealing connection between warehouse independence and view complements. Moreover, we study special kinds of complements, namely monotonic complements, and show how to compute minimal ones in the presence of keys and foreign keys in the underlying databases. Taking advantage of these complements, an algorithmic approach is proposed for the specification of independent warehouses with respect to given sets of queries and updates. Received: 21 November 2000 / Accepted: 1 May 2001 Published online: 6 September 2001     

A logical view of structured files

Structured data stored in files can benefit from standard database technology. In particular, we show here how such data can be queried and updated using declarative database languages. We introduce the notion of structuring schema, which consists of a grammar annotated with database programs. Based on a structuring schema, a file can be viewed as a database structure, queried and updated as such. For queries, we show that almost standard database optimization techniques can be used to answer queries without having to construct the entire database. For updates, we study in depth the propagation to the file of an update specified on the database view of this file. The problem is not feasible in general and we present a number of negative results. The positive results consist of techniques that allow to propagate updates efficiently under some reasonable locality conditions on the structuring schemas. Received November 1, 1995 / Accepted June 20, 1997     

A workshop on formal methods education: held at Melbourne Florida in March 1998[5]

The 21st Century Engineering Consortium Workshop was devoted to educational issues in the area of formal methods. This article summarizes opinions and perspectives which emerged at the workshop and sketches a context for their assessment. There was broad agreement that advances in education are crucial to expanding formal methods practice. However, specific recommendations vary among interest groups and individuals. In this multi-faceted area, it is important to establish a framework for debating issues and presenting them to the broader community. Nowhere is this need greater than in discussions of education.     

Efficient debugging in a formal verification environment

In this paper, we emphasize the importance of efficient debugging in formal verification and present capabilities that we have developed in order to aid debugging in Intel’s Formal Verification Environment. We have given the name “Counter-Example Wizard” to the bundle of capabilities that we have developed to address the needs of the verification engineer in the context of counter-example diagnosis and rectification. The novel features of the Counter-Example Wizard are the multi-value counter-example annotation, constraint-based debugging, and multiple counter-example generation mechanisms. Our experience with the verification of real-life Intel designs shows that these capabilities complement one another and can help the verification engineer diagnose and fix a reported failure. We use real-life verification cases to illustrate how our system solution can significantly reduce the time spent in the loop of model checking, specification, and design modification. Published online: 21 February 2003     

Refinement-based formal verification with heterogeneous timing

In this paper we propose a refinement-based technique to formally verify data transfer in a heterogeneous timing framework. Novel data transfer models are proposed to represent data communication between two locally independent clock domains via an asynchronous handshake environment. As a case study, we apply our technique to automatically verify data transfer in a previously published architecture for globally asynchronous locally synchronous on-chip systems. In this case study, we find several race conditions, hazards, and other dangers that were not mentioned in the original publication, and we find additional delay constraints that avoid some of the detected dangers. Published online: 17 December 2002     

Applying evolutionary algorithms to materialized view selection in a data warehouse

Effective analysis of genome sequences and associated functional data requires access to many different kinds of biological information. A data warehouse [14,16] plays an important role for storage and analysis for genome sequence and functional data. A data warehouse stores lots of materialized views to provide an efficient decision-support or OLAP queries. The view-selection problem addresses to select a fittest set of materialized views from a variety of MVPPs 0 forms a challenge in data warehouse research. In this paper, we present genetic algorithm to choose materialized views. We also use experiments to demonstrate the power of our approach. We would like to thank the authors, i.e. J. Yang, K. Karlapalem, and Q. Li, of the paper [15]. In this study, we borrow their mathematical model of the work in [15].     

VSE: formal methods meet industrial needs

The Verification Support Environment (VSE) is a tool to formally specify and verify complex systems. It provides the means to structure specifications and supports the development process from the specification of a system to the automatic generation of code. Formal developments following the VSE method are stored and maintained in an administration system that guides the user and maintains a consistent state of development. An integrated deduction system provides proof support for the deduction problems arising during the development process. We describe the application of VSE to an industrial case study and give an overview of the enhanced VSE system and the VSE methodology.     

Proof engineering in the large: formal verification of Pentium®4 floating-point divider

We examine the challenges presented by large-scale formal verification of industrial-size circuits, based on our experiences in verifying the class of all micro-operations executing on the floating-point division and square root unit of the Intel IA-32 Pentium?4 microprocessor. The verification methodology is based on combining human-guided mechanised theorem-proving with low-level steps verified by fully automated model-checking. A key observation in the work is the need to explicitly address the issues of proof design and proof engineering, i.e., the process of creating proofs and the craft of structuring and formulating them, as concerns on their own right. Published online: 19 November 2002     

Control and data abstraction: the cornerstones of practical formal verification

In spite of the impressive progress in the development of the two main methods for formal verification of reactive systems – Symbolic Model Checking and Deductive Verification, they are still limited in their ability to handle large systems. It is generally recognized that the only way these methods can ever scale up is by the extensive use of abstraction and modularization, which break the task of verifying a large system into several smaller tasks of verifying simpler systems. In this paper, we review the two main tools of compositionality and abstraction in the framework of linear temporal logic. We illustrate the application of these two methods for the reduction of an infinite-state system into a finite-state system that can then be verified using model checking. The technical contributions contained in this paper are a full formulation of abstraction when applied to a system with both weak and strong fairness requirements and to a general temporal formula, and a presentation of a compositional framework for shared variables and its application for forming network invariants.     

A practical use of cellular neural networks: the stereo-vision problem as an optimisation

A variational way of deriving the relevant parameters of a cellular neural network (CNN) is introduced. The approach exploits the CNN spontaneous internal-energy decrease and is applicable when a given problem can be expressed in terms of an optimisation task. The presented approach is fully mathematical as compared with the typical heuristic search for the correct parameters in the literature on CNNs. This method is practically employed in recovering information on the three-dimensional structure of the environment, through the stereo vision problem. A CNN able to find the conjugate points in a stereogram is fully derived in the proposed framework. Results of computer simulations on several test cases are provided. Received: 1 August 1997 / Accepted: 29 September 1999     

An algorithm for the asynchronous Write-All problem based on process collision

Summary. The problem of using P processes to write a given value to all positions of a shared array of size N is called the Write-All problem. We present and analyze an asynchronous algorithm with work complexity , where (assuming and ). Our algorithm is a generalization of the naive two-processor algorithm where the two processes each start at one side of the array and walk towards each other until they collide. Received: October 1999 / Accepted: September 2000     

Accessibility in the built and transport environment The wheelchair user perspective

‘Improving Accessidility for those with Impaired Mobility’ (I-AIM) is developing a telematic-based device to attach to wheelchairs to provide a navigation aid in the built environment. A technical project such as this must have end-user input from the beginning. In partial fulfilment of this, a user requirements survey was carried out. The survey found that accessibility in the built environment is generally possible for wheelchair users with assistance, which does not fulfil objectives of independence. Accessibility to public transport is regarded as poor. Information communication technologies can offer greater independence and inclusion, but attention must be paid to ergonomics. Published online: 9 October 2001     

Management of access through biometric control: A case study based on automatic signature verification

The idea of the information society is pervasive and varied and, in this context, universal access is itself a multi-faceted concept. However, the notion of universality presupposes an analysis and understanding of what both unifies and discriminates among different individual members of a community of technology users. This paper addresses these ideas and, in particular, seeks to illustrate some techniques which can support such an analysis in a variety of task domains. Of special interest here is a specific case study which examines the use of biometric processing as a means of managing access in the broadest sense. It is argued that not only is the field of biometric measurement one where understanding similarities and differences is the essence of what is required, but also that this offers the opportunity to establish and explore a variety of practical techniques of very wide significance in the context of universal access. Published online: 18 May 2001     

Global transaction support for workflow management systems: from formal specification to practical implementation

In this paper, we present an approach to global transaction management in workflow environments. The transaction mechanism is based on the well-known notion of compensation, but extended to deal with both arbitrary process structures to allow cycles in processes and safepoints to allow partial compensation of processes. We present a formal specification of the transaction model and transaction management algorithms in set and graph theory, providing clear, unambiguous transaction semantics. The specification is straightforwardly mapped to a modular architecture, the implementation of which is first applied in a testing environment, then in the prototype of a commercial workflow management system. The modular nature of the resulting system allows easy distribution using middleware technology. The path from abstract semantics specification to concrete, real-world implementation of a workflow transaction mechanism is thus covered in a complete and coherent fashion. As such, this paper provides a complete framework for the application of well-founded transactional workflows. Received: 16 November 1999 / Accepted 29 August 2001 Published online: 6 November 2001