UB2SQL: A Tool for Building Database Applications Using UML and B Formal Method

UB2SQL: A Tool for Building Database Applications Using UML and B Formal Method

Amel Mammar (University of Paris, France)
DOI: 10.4018/978-1-60566-172-8.ch007
OnDemand PDF Download:


UB2SQL is a tool for designing and developing database applications using UML and B formal method. The approach supported by UB2SQL consists of two successive phases. In the first phase, with the design of applications using class, state and collaboration diagrams, B specifications are automatically generated from UML diagrams; the diagrams are then augmented with these B specifications in place. The second phase deals with the refinement of these B specifications into a relational database implementation, for which UML representation is constructed. In both phases, proofs are achieved to ensure correctness of the obtained B specification and correctness of the refinement process. To overcome the lack of rules and tactics in the B prover, UB2SQL defines specific rules and tactics making the proof task seem like a push-button activity. To increase the usability of UB2SQL in both academic and industrial contexts, the tool has been integrated as a plug-in to the Rational Rose CASE tool. Such integration allows users to develop and be able to visualize graphical UML diagrams and formal B notation in a single environment.
Chapter Preview


In the area of database specification and design, most research work has been dedicated to data modeling through the definition of the Entity-Relationship (ER) model and its variants. Formal rules are designed to translate ER diagrams into database schemas and included as part of the functionality of existing industrial CASE tools. This principle has not yet been applied to database transaction design, even though some research work in that direction has been carried out (Barros, 1998; Edmond, 1995; Gunther, Schewe, and Wetzel, 1993). A couple of reasons for this should be mentioned. First, in this kind of application, data are the core component and their modeling requires much attention (since the quality of the built system mainly depends on this modeling). Second, specifying database transactions at the same abstraction level as the ER model requires the use of formal specification notations such as B (Abrial, 1996), VDM (Jones, 1990) or Z (Spivey, 1992); however, the use of formal methods raises some difficulties, as pointed out in a survey performed on experienced formal methods users (Snook and Butler, 2006). The survey observes that reading and understanding formal specifications is not a significant problem with suitable training; the main difficulty lies in creating formal specifications, and more precisely in finding useful abstractions like choosing the objects that make up the model. The authors conclude by recommending that formal methods should be more closely integrated with classical design methods, such as UML (OMG, 2003; Siau and Cao, 2001; Siau and Lee, 2004; Siau, Erickson, and Lee, 2005), which have been successfully used to design programs, and that graphical modeling tools supporting such integrations should be developed. Thus, a number of research projects (Bruel and France, 1996; Dupuy, Ledru, and Chabre-Peccoud, 2000; Ledang, Souquieres, and Charles, 2003; Marcano and Levy, 2002; Snook and Butler, 2006) have been devoted to such purpose. Formal proofs are another theme in formal methods. The objective is to increase the degree of proof-automation. A possible approach is to develop domain-dedicated provers and tools (Bernard, Legeard, Luck, and Peureux, 2004).

Our research work is at the junction of these themes and our aim is to define a method for the specification and design of database applications supported by a graphical modeling tool. In our proposal, data are first specified using UML class diagrams; transactions are then modeled with state and collaboration diagrams augmented with formal semantics. These adapted UML diagrams are converted into B specifications, which are then refined into a relational database implementation. The B method (Abrial, 1996) is a safe technique that covers the different phases of the software development life cycle: abstract specification, design by successive refinement steps and executable code generation. Using the B method, database engineers are able to check that transactions preserve integrity constraints expressed in the abstract specification. With the integration of UML+B, we can take advantage of the visual and structuring aspects of UML graphical notation, together with the rigorous reasoning possibilities of B formal notation. This paper focuses on the construction of the tool, UB2SQL, which supports our approach (UML+B). We highlight the main functionalities of UB2SQL, how it is integrated as a plug-in to the Rose CASE tool (Rational, 2003) and list the issues faced during its construction. Finally, we conclude by giving some quantitative elements and pointing out the advantages of such a tool. More details on the method itself can be found in our previous work (Laleau and Mammar, 2000a; 2000b, 2005; Mammar, 2002).

Complete Chapter List

Search this Book:
Editorial Advisory Board
Table of Contents
Chapter 1
Hong Zhang, Rajiv Kishore, Ram Ramesh
A conceptual modeling grammar should be based on the theory of ontology and possess clear ontological semantics to represent problem domain... Sample PDF
Semantics of the MibML Conceptual Modeling Grammar: An Ontological Analysis Using the Bunge-Wand-Weber Framework
Chapter 2
Henry M. Kim, Arijit Sengupta, Mark S. Fox, Mehmet Dalkilic
This paper introduces a measurement ontology for applications to semantic Web applications, specifically for emerging domains such as microarray... Sample PDF
A Measurement Ontology Generalizable for Emerging Domain Applications on the Semantic Web
Chapter 3
Zhiyuan Chen
Environmental research and knowledge discovery both require extensive use of data stored in various sources and created in different ways for... Sample PDF
Semantic Integration and Knowledge Discovery for Environmental Research
Chapter 4
Vijayan Sugumaran, Gerald DeHondt
Software reuse has been discussed in the literature for the past three decades and is widely seen as one of the major areas for improving... Sample PDF
Towards Code Reuse and Refactoring as a Practice within Extreme Programming
Chapter 5
Miguel I. Aguiree-Urreta, George M. Marakas
Requirements elicitation has been recognized as a critical stage in system development projects, yet current models prescribing particular... Sample PDF
Requirements Elicitation Technique Selection: A Theory-Based Contingency Model
Chapter 6
VenuGopal Balijepally, Sridhar Nerur, RadhaKanta Mahapatra
Software development in organizations is evolving and increasingly taking a socio-technical hue. While empirical research guided by common sense... Sample PDF
IT Value of Software Development: A Multi-Theoretic Perspective
Chapter 7
Amel Mammar
UB2SQL is a tool for designing and developing database applications using UML and B formal method. The approach supported by UB2SQL consists of two... Sample PDF
UB2SQL: A Tool for Building Database Applications Using UML and B Formal Method
Chapter 8
Juliette Gutierrez
Crime reports are used to find criminals, prevent further violations, identify problems causing crimes and allocate government resources.... Sample PDF
Using Decision Trees to Predict Crime Reporting
Chapter 9
Karen Corral, David Schuff, Robert D. St. Louis, Ozgur Turetken
Inefficient and ineffective search is widely recognized as a problem for businesses. The shortcomings of keyword searches have been elaborated upon... Sample PDF
A Model for Estimating the Savings from Dimensional vs. Keyword Search
Chapter 10
Praveen Madiraju, Rajshekhar Sunderraman, Shamkant B. Navathe, Haibin Wang
Global semantic integrity constraints ensure the integrity and consistency of data spanning distributed databases. In this chapter, we discuss a... Sample PDF
Integrity Constraint Checking for Multiple XML Databases
Chapter 11
Russel Pears
Data Warehouses are widely used for supporting decision making. On Line Analytical Processing or OLAP is the main vehicle for querying data... Sample PDF
Accelerating Multi Dimensional Queries in Data Warehouses
Chapter 12
Vikas Agrawal, P. S. Sundararaghavan, Mesbah U. Ahmed, Udayan Nandkeolyar
Data warehouse has become an integral part in developing a DSS in any organization. One of the key architectural issues concerning the efficient... Sample PDF
View Materialization in a Data Cube: Optimization Models and Heuristics
Chapter 13
Athman Bouguettaya, Zaki Malik, Xumin Liu, Abdelmounaam Rezgui, Lori Korff
The ubiquity of the World Wide Web facilitates the deployment of highly distributed applications. The emergence of Web databases and applications... Sample PDF
WebFINDIT: Providing Data and Service-Centric Access through a Scalable Middleware
Chapter 14
James E. Wyse
Location-based mobile commerce (LBMC) incorporates location-aware technologies, wire-free connectivity, and server-based repositories of business... Sample PDF
Retrieval Optimization for Server-Based Repositories in Location-Based Mobile Commerce
Chapter 15
Shing-Han Li, Shi-Ming Huang, David C. Yen, Cheng-Chun Chang
The lifecycle of information system (IS) became relatively shorter compared with earlier days as a result of information technology (IT) revolution... Sample PDF
Migrating Legacy Systems to Web Services Architecture
Chapter 16
Myeong Ho Lee
The trend toward convergence, initiated by advances in ICT, entails the creation of new value chain networks, made up by partnerships between actors... Sample PDF
A Socio-Technical Interpretation of IT Convergence Services: Applying a Perspective from Actor Network Theory and Complex Adaptive Systems
Chapter 17
T. Ariyachandra, L. Dong
Past evidence suggests that organizational transformation from IT implementations is rare. Data warehousing promises to be one advanced information... Sample PDF
Understanding Organizational Transformation from IT Implementations: A Look at Structuration Theory
Chapter 18
Yuan Long, Keng Siau
Drawing on social network theories and previous studies, this research examines the dynamics of social network structures in Open Source Software... Sample PDF
Social Networks Structures in Open Source Software Development Teams
Chapter 19
Susanta Mitra, Aditya Bagchi, A. K. Bandyopadhyay
A social network defines the structure of a social community like an organization or institution, covering its members and their... Sample PDF
Design of a Data Model for Social Networks Applications
About the Contributors