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.

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.

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.

Minkowski Operators and Features of Voxel Models

1999 ◽  
Author(s):  
V. Chandru ◽  
M. Manivannan ◽  
S. Manohar
Keyword(s):  
Data Structures ◽  
Structural Information ◽  
Prototype System ◽  
Cad Systems ◽  
Feature Based ◽  
Data Structures And Algorithms ◽  
Feature Based Design ◽  
Traditional Representation

Abstract Feature-based design has evolved as a fundamental paradigm for present-day CAD systems. Voxel-based modeling has many advantages over traditional representation schemes but lacks structural information which is lost in voxelization of the objects. In this paper, we propose to augment voxel models with features by a) storing the sequence of modeling operations along with voxel models and b) by defining feature operators. We have implemented these ideas in our prototype system Sirpi as regularised Minkowski operators using simple data structures and algorithms.

Sign in / Sign up

Export Citation Format

Share Document