ASM-based design of data warehouses and on-line analytical processing systems

On-line analytical processing (OLAP) systems deal with analytical tasks in businesses. As these tasks do not depend on the latest updates by transactions, it is assumed that the data used in OLAP systems are kept in a data warehouse, which separates the input from operational databases from the outputs to dialogue interfaces for OLAP. Data Warehouses and OLAP systems are a promising area for the application of Abstract State Machines (ASMs). In this article a layered ground model specification for data warehouses and OLAP system is presented that is based explicitly on the fundamental idea of separating input from operational databases from output to OLAP systems. On this basis we start defining formal refinement rules for such systems. As these refinement rules are formally correct they enable a formal method for the high-quality design of data warehouses and OLAP systems that can be applied without knowing mathematical details of the ASM formalism. Furthermore, we discuss pragmatic guidelines for the application of such rules.