Database Design Based on B

2009 ◽  
pp. 440-456 ◽  
Author(s):  
Elvira Locuratolo
Keyword(s):  
Data Structures ◽  
Formal Method ◽  
Real Life ◽  
Database Design ◽  
Model Transformations ◽  
Software Systems ◽  
The Novel ◽  
Life Changes ◽  
Semantic Data ◽  
Object Models

This chapter is devoted to the integration of the ASSO features in B. ASSO is a database design methodology defined for achieving conceptual schema consistency, logical schema correctness, flexibility in reflecting the real-life changes on the schema and efficiency in accessing and storing information. B is an industrial formal method for specifying, designing, and coding software systems. Starting from a B specification of the data structures and of the transactions allowed on a database, two model transformations are designed: The resulting model, called Structured Database Schema, integrates static and dynamics exploiting the novel concepts of Class-Machine and Specialized Class-Machine. Formal details which must be specified if the conceptual model of ASSO is directly constructed in B are avoided; the costs of the consistency obligations are minimized. Class-Machines supported by semantic data models can be correctly linked with Class-Machines supported by object Models.

Database Design Based on B

2011 ◽  
pp. 35-61
Author(s):  
Elvira Locuratolo
Keyword(s):  
Data Structures ◽  
Formal Method ◽  
Real Life ◽  
Database Design ◽  
Model Transformations ◽  
Software Systems ◽  
The Novel ◽  
Life Changes ◽  
Semantic Data ◽  
Object Models

This chapter is devoted to the integration of the ASSO features in B. ASSO is a database design methodology defined for achieving conceptual schema consistency, logical schema correctness, flexibility in reflecting the real-life changes on the schema and efficiency in accessing and storing information. B is an industrial formal method for specifying, designing, and coding software systems. Starting from a B specification of the data structures and of the transactions allowed on a database, two model transformations are designed: The resulting model, called Structured Database Schema, integrates static and dynamics exploiting the novel concepts of Class-Machine and Specialized Class-Machine. Formal details which must be specified if the conceptual model of ASSO is directly constructed in B are avoided; the costs of the consistency obligations are minimized. Class-Machines supported by semantic data models can be correctly linked with Class-Machines supported by object Models.

Model Transformations in Designing the ASSO Methodology

2011 ◽  
pp. 283-302 ◽  
Author(s):  
Elvira Locuratolo
Keyword(s):  
Formal Method ◽  
Dynamic Modelling ◽  
Data Models ◽  
Model Transformations ◽  
Conceptual Schema ◽  
Behavioural Modelling ◽  
Semantic Data ◽  
Object Models ◽  
Consistency Proofs ◽  
Formal Mapping

ASSO, an innovative conceptual methodology which combines features of database design with the formal method B, has been defined in order to ensure the flexibility of semantic data models, the efficiency of object models and design correctness. Starting from a directed acyclic graph of classes supported by semantic data models, a formal mapping generates classes supported by object models. The classes supported by semantic data models are then extended with aspects of behavioural modelling: a relationship with the B model is established and the consistency proofs of the whole schema are reduced to small obligations of B. This chapter evidences how ASSO is based on model transformations. These have been introduced with various purposes: to map semantic data models to object models, to integrate static and dynamic modelling, to link formal and informal notations and to relate the conceptual schema and the logical schema of the methodology.

MODELING AND VERIFYING COMPOSITE DYNAMIC EVOLUTION OF SOFTWARE ARCHITECTURES USING HYPERGRAPH GRAMMARS

2013 ◽  
Vol 23 (06) ◽  
pp. 775-799 ◽  
Author(s):  
HONGZHEN XU ◽  
GUOSUN ZENG
Keyword(s):  
Data Structures ◽  
Formal Method ◽  
Graphical Representation ◽  
General Structure ◽  
Software Systems ◽  
Dynamic Evolution ◽  
Software Architectures ◽  
Model Composite ◽  
Verification Algorithms ◽  
Data Structures And Algorithms

As software systems become more and more complex, there is need to consider not only data structures and algorithms but also the general structure or architecture of the system. Many researchers have presently focused on dynamic evolution of software architectures. Most of them usually emphasized on describing and analyzing the dynamic evolution process of software architectures, while lacking formally modeling and verifying composite dynamic evolution of software architectures. In this paper, we propose a formal method of modeling and verifying composite dynamic evolution of software architectures using hypergraph grammars. We represent software architectures with hypergraphs, give out corresponding composite evolution rules of software architectures, and then model composite dynamic evolution of software architectures according to those rules. At last we verify the liveness property of composite dynamic evolution of software architectures using model checking, and give out corresponding verification algorithms. Our approach provides a graphical representation for composite dynamic evolution of software architectures, and displays a formal theoretical basis on grammars.

A NOVEL APPROACH TO VERIFY GRAPH SCHEMA-BASED SOFTWARE SYSTEMS

2009 ◽  
Vol 19 (06) ◽  
pp. 857-870 ◽  
Author(s):  
VAHID RAFE ◽  
ADEL T. RAHMANI
Keyword(s):  
Graph Transformation ◽  
Behavioral Modeling ◽  
Model Transformations ◽  
Software Systems ◽  
Hierarchical Systems ◽  
Input Language ◽  
Novel Approach ◽  
Graph Schema ◽  
Transformation Systems ◽  
Graph Transformation Systems

Graph Grammars have recently become more and more popular as a general formal modeling language. Behavioral modeling of dynamic systems and model to model transformations are a few well-known examples in which graphs have proven their usefulness in software engineering. A special type of graph transformation systems is layered graphs. Layered graphs are a suitable formalism for modeling hierarchical systems. However, most of the research so far concentrated on graph transformation systems as a modeling means, without considering the need for suitable analysis tools. In this paper we concentrate on how to analyze these models. We will describe our approach to show how one can verify the designed graph transformation systems. To verify graph transformation systems we use a novel approach: using Bogor model checker to verify graph transformation systems. The AGG-like graph transformation systems are translated to BIR — the input language of Bogor — and Bogor verifies that model against some properties defined by combining LTL and special purpose graph rules. Supporting schema-based and layered graphs characterize our approach among existing solutions for verification of graph transformation systems.

Integrating Image Computation in Undergraduate Level Data-Structure Education

1998 ◽  
Vol 12 (08) ◽  
pp. 1071-1080 ◽  
Author(s):  
Sudeep Sarkar ◽  
Dmitry Goldgof
Keyword(s):  
Image Processing ◽  
Image Analysis ◽  
Data Structure ◽  
Data Structures ◽  
Science Curriculum ◽  
Early Stage ◽  
Real Life ◽  
South Florida ◽  
The University ◽  
Structure Education

There is a growing need for expertise both in image analysis and in software engineering. To date, these two areas have been taught separately in an undergraduate computer and information science curriculum. However, we have found that introduction to image analysis can be easily integrated in data-structure courses without detracting from the original goal of teaching data structures. Some of the image processing tasks offer a natural way to introduce basic data structures such as arrays, queues, stacks, trees and hash tables. Not only does this integrated strategy expose the students to image related manipulations at an early stage of the curriculum but it also imparts cohesiveness to the data-structure assignments and brings them closer to real life. In this paper we present a set of programming assignments that integrates undergraduate data-structure education with image processing tasks. These assignments can be incorporated in existing data-structure courses with low time and software overheads. We have used these assignment sets thrice: once in a 10-week duration data-structure course at the University of California, Santa Barbara and the other two times in 15-week duration courses at the University of South Florida, Tampa.

scholarly journals Algorithmic Transparency of Large-Scale *AIDA Programs

2020 ◽  
Vol 30 (09) ◽  
pp. 1263-1288
Author(s):  
Yutaka Watanobe ◽  
Nikolay Mirenkov
Keyword(s):  
Data Structures ◽  
Large Scale ◽  
Software Systems ◽  
Computational Algorithms ◽  
Computer Language ◽  
Algorithms And Data Structures ◽  
Application Methods ◽  
Analysis System ◽  
Computational Comparison

Programming in pictures is an approach where pictures and moving pictures are used as super-characters to represent the features of computational algorithms and data structures, as well as for explaining the models and application methods involved. *AIDA is a computer language that supports programming in pictures. This language and its environment have been developed and promoted as a testbed for various innovations in information technology (IT) research and implementation, including exploring the compactness of the programs and their adaptive software systems, and obtaining better understanding of information resources. In this paper, new features of the environment and methods of their implementation are presented. They are considered within a case study of a large-scale module of a nuclear safety analysis system to demonstrate that *AIDA language is appropriate for developing efficient codes of serious applications and for providing support, based on folding/unfolding techniques, enhancing the readability, maintainability and algorithmic transparency of programs. Features of this support and the code efficiency are presented through the results of a computational comparison with a FORTRAN equivalent.

scholarly journals Woman’s Suppression in Azab dan Sengsara: A Feminist Perspective

2017 ◽  
Vol 4 (1) ◽  
pp. 37-51
Author(s):  
Siti Hafsah
Keyword(s):  
Qualitative Method ◽  
Real Life ◽  
Feminist Perspective ◽  
Material Object ◽  
The Novel ◽  
Literary Sociology ◽  
A Company

Azab dan Sengsara is an Indonesian novel written by Merari Siregar (1921), one of the famous roman novelists in Indonesia in Balai Pustaka era. The novel is a material object of the present study. The study aims at revealing oppression, violence, exploitation of woman and all varieties of injustice to woman, revealing social symptoms ideological forms containing in the novel as a manifestation of a company condition in old era. This research uses a qualitative method and approaches of literary feminist and literary sociology as its support. This research succeeds in answering the problems of woman life, as manifestation of real life which reflects kinds of woman’s life in society of Indonesian, for example: marriage, custom, violence, etc. for the hero “Mariamin” (a woman). She is the manifestation of the authority life, besides talking on oppression of woman images of its community lives. The author succeeded offering solutions with various contradictions, conflicts, handling down the novel as manifestation in real life.

scholarly journals Tilsynekomstens politik. Om virkelighedsmodellering i Joseph Conrads Nostromo

2011 ◽  
Vol 39 (111) ◽  
pp. 7-26
Author(s):  
Jonas Kjærgård Laursen
Keyword(s):  
Real Life ◽  
The Novel ◽  
Human Consciousness ◽  
Politics And Literature ◽  
Ideological Criticism ◽  
Jacques Ranciere ◽  
Politics Of Literature ◽  
Material Interests ◽  
Political Problem ◽  
Novelistic Form

POLITICS OF APPEARANCE. ON REALITY MODELLING IN JOSEPH CONRAD’S NOSTROMOArtistically Nostromo is arguably the most ambitious of Joseph Conrad’s novels. It is also without a doubt the most explicitly political in that it openly engages with the question of how capitalism, imperialism, and revolution affect the human consciousness. There is however no agreement as to how this political problem is to be understood or, more precisely, what kind of understanding of the interrelationship between politics and literature is necessary when engaging this artwork. As a necessary supplement to both a 60’s Marxist reading and readings from the 70’s and 80’s dealing with ideological criticism, this article suggests a reading focusing on how the text creates a model of society by reconfiguring certain real life elements. By developing a specific artistic idiom Nostromo attempts to show the very limited view of the whole of society caused by, in the wording of the novel, the material interests of imperial capitalism. Under the inspiration of both Jurij Lotman and Jacques Rancière the analysis presented here is able to address some key political insights that appear as a consequence of the novelistic form when understood as a relatively autonomous model of society. And that is what is meant by the expression politics of appearance: the politics of literature is to be analysed as something generated by the specific gestalt of the text, as something that comes into sight with – and only with – the text.

scholarly journals NORMALIZATION IN DATABASE DESIGN

2018 ◽  
Vol 4 (1) ◽  
pp. 34
Author(s):  
Zainul Efendy
Keyword(s):  
Data Structures ◽  
Query Language ◽  
Database Design ◽  
Simple Solution ◽  
Transaction Model ◽  
Model Form

This research is done to find a simple solution how to find a normalization techniques are appropriate in database design, normalization techniques has several steps of which are forms of abnormal, normalization first, normalization 2st and normalization 3st, only 3 stages rare to be discussed in this study, as in lectures often find their students do not understand to implement this normalization techniques. The results of this study include determining the database data structures, forming sql (structural query language) by using MySQL DBMS and prototype transaction model form.

scholarly journals Filmed Monologue Vignettes: a novel method for investigating how clinicians document consultations in electronic health records

2018 ◽  
Vol 3 (1) ◽  
Author(s):  
Simon Glew ◽  
Elizabeth M Ford ◽  
Helen Elizabeth Smith
Keyword(s):  
Real Life ◽  
Correct Selection ◽  
Free Text ◽  
The Novel ◽  
Face To Face ◽  
Full Compliance ◽  
Electronic Healthcare Record ◽  
Novel Method ◽  
Quality Rating ◽  
Selection Of Descriptors

Introduction and Objectives The accuracy of conclusions based on Electronic Healthcare Record (EHR) research is highly dependent on the correct selection of descriptors (codes) by users. We aimed to evaluate the feasibility and acceptability of filmed vignette monologues as a resource-light method of assessing and comparing how different EHR users record the same clinical scenario. Methods Six short monologues of actors portraying patients presenting allergic conditions to their General Practitioners were filmed head-on then electronically distributed for the study; no researcher was present during data collection. The method was assessed by participant uptake, reported ease of completion by participants, compliance with instructions, the receipt of interpretable data by researchers, and participant perceptions of vignette quality, realism and information content. Results 22 participants completed the study, reporting only minor difficulties. 132 screen prints were returned electronically, enabling analysis of codes, free text and EHR features. Participants assigned a quality rating of 7.7/10 (range 2-10) to the vignettes and rated the extent to which vignettes reflected real-life (86-100%). Between 1 and 2 hours were required to complete the task. Full compliance with instructions varied between participants but was largely successful. Conclusions Filmed monologues are a reproducible, standardized method which require few resources, yet allow clear assessment of clinicians’ and EHRs systems’ impact on documentation. The novel nature of this method necessitates clear instructions so participants can fully complete the study without face to face researcher oversight.

Sign in / Sign up

Export Citation Format

Share Document