The Formal Design Models of Tree Architectures and Behaviors

2011 ◽  
Vol 3 (4) ◽  
pp. 84-108 ◽  
Author(s):  
Yingxu Wang ◽  
Xinming Tan
Keyword(s):  
Real Time ◽  
Hierarchical Structures ◽  
General System ◽  
Process Models ◽  
Behavioral Models ◽  
Code Generator ◽  
Organization Model ◽  
B Trees ◽  
Left And Right ◽  
Automatic Code

Trees are one of the most fundamental and widely used non-linear hierarchical structures of linked nodes. A binary tree (B-Tree) is a typical balanced tree where the fan-out of each node is at most two known as the left and right children. This paper develops a comprehensive design pattern of formal trees using the B-Tree architecture. A rigorous denotational mathematics, Real-Time Process Algebra (RTPA), is adopted, which allows both architectural and behavioral models of B-Trees to be rigorously designed and implemented in a top-down approach. The architectural models of B-Trees are created using RTPA architectural modeling methodologies known as the Unified Data Models (UDMs). The physical model of B-Trees is implemented using the left and right child nodes dynamically created in memory. The behavioral models of B-Trees are specified and refined by a set of Unified Process Models (UPMs) in three categories namely the management operations, traversal operations, and node I/O operations. This work has been applied in a number of real-time and nonreal-time system designs such as a real-time operating system (RTOS+), a general system organization model, and the ADT library for an RTPA-based automatic code generator.

The Formal Design Models of Tree Architectures and Behaviors

2013 ◽  
pp. 260-281
Author(s):  
Yingxu Wang ◽  
Xinming Tan
Keyword(s):  
Real Time ◽  
Hierarchical Structures ◽  
Process Models ◽  
Behavioral Models ◽  
Code Generator ◽  
Organization Model ◽  
B Trees ◽  
Left And Right ◽  
Balanced Tree ◽  
Automatic Code

Trees are one of the most fundamental and widely used non-linear hierarchical structures of linked nodes. A binary tree (B-Tree) is a typical balanced tree where the fan-out of each node is at most two known as the left and right children. This paper develops a comprehensive design pattern of formal trees using the B-Tree architecture. A rigorous denotational mathematics, Real-Time Process Algebra (RTPA), is adopted, which allows both architectural and behavioral models of B-Trees to be rigorously designed and implemented in a top-down approach. The architectural models of B-Trees are created using RTPA architectural modeling methodologies known as the Unified Data Models (UDMs). The physical model of B-Trees is implemented using the left and right child nodes dynamically created in memory. The behavioral models of B-Trees are specified and refined by a set of Unified Process Models (UPMs) in three categories namely the management operations, traversal operations, and node I/O operations. This work has been applied in a number of real-time and nonreal-time system designs such as a real-time operating system (RTOS+), a general system organization model, and the ADT library for an RTPA-based automatic code generator.

The Formal Design Models of Digraph Architectures and Behaviors

2012 ◽  
Vol 4 (1) ◽  
pp. 100-129 ◽  
Author(s):  
Yingxu Wang ◽  
Aderemi Adewumi
Keyword(s):  
Real Time ◽  
Code Generation ◽  
Graph Model ◽  
Hierarchical Structures ◽  
Process Models ◽  
Behavioral Models ◽  
Complicated Form ◽  
Architectural Models ◽  
Automatic Code ◽  
Formal Design

Graphs are one of the most fundamental and widely used non-linear hierarchical structures of linked nodes. Problems in sciences and engineering can be formulated and solved by the graph model. This paper develops a comprehensive design pattern of formal digraphs using the Doubly-Linked List (DLL) architecture. The most complicated form of graphs known as the weighted digraph is selected as a general graph model, based on it simple graphs such as nondirected and/or nonweighted ones can be easily derived and tailored. A rigorous denotational mathematics, Real-Time Process Algebra (RTPA), is adopted, which allows both architectural and behavioral models of digraphs to be rigorously designed and implemented in a top-down approach. The architectural models of digraphs are created using RTPA architectural modeling methodologies known as the Unified Data Models (UDMs). The physical model of digraphs is implemented using nodes of DLL dynamically created in the memory. The behavioral models of digraphs are specified and refined by a set of 18 Unified Process Models (UPMs) in three categories namely the management operations, traversal operations, and node manipulation operations. This work has been applied in a number of real-time and nonreal-time system designs and specifications such as a Real-Time Operating System (RTOS+), graph-based and tree-based applications, and the ADT library for an RTPA-based automatic code generation tool.

The Formal Design Models of a Universal Array (UA) and its Implementation

2011 ◽  
Vol 3 (3) ◽  
pp. 69-89 ◽  
Author(s):  
Yingxu Wang ◽  
Jason Huang ◽  
Jingsheng Lei
Keyword(s):  
Real Time ◽  
Code Generation ◽  
Formal Model ◽  
Process Models ◽  
Behavioral Models ◽  
Universal Array ◽  
Linear List ◽  
Data Objects ◽  
Automatic Code ◽  
Formal Design

Arrays are one of the most fundamental and widely applied data structures, which are useful for modeling both logical designs and physical implementations of multi-dimensional data objects sharing the same type of homogeneous elements. However, there is a lack of a formal model of the universal array based on it any array instance can be derived. This paper studies the fundamental properties of Universal Array (UA) and presents a comprehensive design pattern. A denotational mathematics, Real-Time Process Algebra (RTPA), allows both architectural and behavioral models of UA to be rigorously designed and refined in a top-down approach. The conceptual model of UA is rigorously described by tuple- and matrix-based mathematical models. The architectural models of UA are created using RTPA architectural modeling methodologies known as the Unified Data Models (UDMs). The physical model of UA is implemented using linear list that is indexed by an offset pointer of elements. The behavioral models of UA are specified and refined by a set of Unified Process Models (UPMs). As a case study, the formal UA models are implemented in Java. This work has been applied in a number of real-time and nonreal-time systems such as compilers, a file management system, the real-time operating system (RTOS+), and the ADT library for an RTPA-based automatic code generation tool.

The Formal Design Models of a Universal Array (UA) and its Implementation

2013 ◽  
pp. 241-259
Author(s):  
Yingxu Wang ◽  
Jason Huang ◽  
Jingsheng Lei
Keyword(s):  
Real Time ◽  
Code Generation ◽  
Formal Model ◽  
Process Models ◽  
Behavioral Models ◽  
Universal Array ◽  
Linear List ◽  
Data Objects ◽  
Automatic Code ◽  
Formal Design

Arrays are one of the most fundamental and widely applied data structures, which are useful for modeling both logical designs and physical implementations of multi-dimensional data objects sharing the same type of homogeneous elements. However, there is a lack of a formal model of the universal array based on it any array instance can be derived. This paper studies the fundamental properties of Universal Array (UA) and presents a comprehensive design pattern. A denotational mathematics, Real-Time Process Algebra (RTPA), allows both architectural and behavioral models of UA to be rigorously designed and refined in a top-down approach. The conceptual model of UA is rigorously described by tuple- and matrix-based mathematical models. The architectural models of UA are created using RTPA architectural modeling methodologies known as the Unified Data Models (UDMs). The physical model of UA is implemented using linear list that is indexed by an offset pointer of elements. The behavioral models of UA are specified and refined by a set of Unified Process Models (UPMs). As a case study, the formal UA models are implemented in Java. This work has been applied in a number of real-time and nonreal-time systems such as compilers, a file management system, the real-time operating system (RTOS+), and the ADT library for an RTPA-based automatic code generation tool.

The Formal Design Model of Doubly-Linked-Circular Lists (DLC-Lists)

2013 ◽  
pp. 214-230
Author(s):  
Yingxu Wang ◽  
Cyprian F. Ngolah ◽  
Xinming Tan ◽  
Phillip C.Y. Sheu
Keyword(s):  
Real Time ◽  
Code Generation ◽  
System Modeling ◽  
Finite Sequence ◽  
Process Models ◽  
Behavioral Models ◽  
Data Types ◽  
Abstract Data ◽  
Automatic Code ◽  
Formal Design

Abstract Data Types (ADTs) are a set of highly generic and rigorously modeled data structures in type theory. Lists as a finite sequence of elements are one of the most fundamental and widely used ADTs in system modeling, which provide a standard encapsulation and access interface for manipulating large-volume information and persistent data. This paper develops a comprehensive design pattern of formal lists using a doubly-linked-circular (DLC) list architecture. A rigorous denotational mathematics, Real-Time Process Algebra (RTPA), is adopted, which allows both architectural and behavioral models of lists to be rigorously designed and implemented in a top-down approach. The architectural models of DLC-Lists are created using RTPA architectural modeling methodologies known as the Unified Data Models (UDMs). The behavioral models of DLC-Lists are specified and refined by a set of Unified Process Models (UPMs) in three categories namely the management operations, traversal operations, and node I/O operations. This work has been applied in a number of real-time and nonreal-time system designs such as a real-time operating system (RTOS+), a file management system (FMS), and the ADT library for an RTPA-based automatic code generation tool.

The Formal Design Model of Doubly-Linked-Circular Lists (DLC-Lists)

2011 ◽  
Vol 3 (2) ◽  
pp. 83-102 ◽  
Author(s):  
Yingxu Wang ◽  
Cyprian F. Ngolah ◽  
Xinming Tan ◽  
Phillip C.Y. Sheu
Keyword(s):  
Real Time ◽  
Code Generation ◽  
System Modeling ◽  
Finite Sequence ◽  
Process Models ◽  
Behavioral Models ◽  
Data Types ◽  
Persistent Data ◽  
Automatic Code ◽  
Formal Design

Abstract Data Types (ADTs) are a set of highly generic and rigorously modeled data structures in type theory. Lists as a finite sequence of elements are one of the most fundamental and widely used ADTs in system modeling, which provide a standard encapsulation and access interface for manipulating large-volume information and persistent data. This paper develops a comprehensive design pattern of formal lists using a doubly-linked-circular (DLC) list architecture. A rigorous denotational mathematics, Real-Time Process Algebra (RTPA), is adopted, which allows both architectural and behavioral models of lists to be rigorously designed and implemented in a top-down approach. The architectural models of DLC-Lists are created using RTPA architectural modeling methodologies known as the Unified Data Models (UDMs). The behavioral models of DLC-Lists are specified and refined by a set of Unified Process Models (UPMs) in three categories namely the management operations, traversal operations, and node I/O operations. This work has been applied in a number of real-time and nonreal-time system designs such as a real-time operating system (RTOS+), a file management system (FMS), and the ADT library for an RTPA-based automatic code generation tool.

The Formal Design Models of a Set of Abstract Data Types (ADTs)

2012 ◽  
pp. 288-315
Author(s):  
Yingxu Wang ◽  
Xinming Tan ◽  
Cyprian F. Ngolah ◽  
Philip Sheu
Keyword(s):  
Real Time ◽  
Cognitive Learning ◽  
Process Models ◽  
Behavioral Models ◽  
Abstract Data Types ◽  
Data Types ◽  
Dynamic Behaviors ◽  
Modeling Methodology ◽  
Abstract Data ◽  
Data Objects

Type theories are fundamental for underpinning data object modeling and system architectural design in computing and software engineering. Abstract Data Types (ADTs) are a set of highly generic and rigorously modeled data structures in type theory. ADTs also play a key role in Object-Oriented (OO) technologies for software system design and implementation. This paper presents a formal modeling methodology for ADTs using the Real-Time Process Algebra (RTPA), which allows both architectural and behavioral models of ADTs and complex data objects. Formal architectures, static behaviors, and dynamic behaviors of a set of ADTs are comparatively studied. The architectural models of the ADTs are created using RTPA architectural modeling methodologies known as the Unified Data Models (UDMs). The static behaviors of the ADTs are specified and refined by a set of Unified Process Models (UPMs) of RTPA. The dynamic behaviors of the ADTs are modeled by process dispatching technologies of RTPA. This work has been applied in a number of real-time and non-real-time system designs such as a Real-Time Operating System (RTOS+), a Cognitive Learning Engine (CLE), and the automatic code generator based on RTPA.

The Formal Design Model of a Lift Dispatching System (LDS)

2009 ◽  
Vol 1 (4) ◽  
pp. 111-137 ◽  
Author(s):  
Yingxu Wang ◽  
Cyprian F. Ngolah ◽  
Hadi Ahmadi ◽  
Philip Sheu ◽  
Shi Ying
Keyword(s):  
Real Time ◽  
Expressive Power ◽  
Process Models ◽  
Software Systems ◽  
Real Time System ◽  
Code Generator ◽  
Design Paradigm ◽  
Process Deployment ◽  
Formal Design ◽  
Priority Allocation

A Lift Dispatching System (LDS) is a typical real-time system that is highly complicated in design and implementation. This article presents the formal design, specification, and modeling of the LDS system using a denotational mathematics known as Real-Time Process Algebra (RTPA). The conceptual model of the LDS system is introduced as the initial requirements for the system. The architectural model of the LDS system is created using RTPA architectural modeling methodologies and refined by a set of Unified Data Models (UDMs). The static behaviors of the LDS system are specified and refined by a set of Unified Process Models (UPMs) for the lift dispatching and serving processes. The dynamic behaviors of the LDS system are specified and refined by process priority allocation and process deployment models. Based on the formal design models of the LDS system, code can be automatically generated using the RTPA Code Generator (RTPA-CG), or be seamlessly transferred into programs by programmers. The formal models of LDS may not only serve as a formal design paradigm of real-time software systems, but also a test bench of the expressive power and modeling capability of exiting formal methods in software engineering.

The Formal Design Model of an Automatic Teller Machine (ATM)

2010 ◽  
Vol 2 (1) ◽  
pp. 102-131 ◽  
Author(s):  
Yingxu Wang ◽  
Yanan Zhang ◽  
Philip C.Y. Sheu ◽  
Xuhui Li ◽  
Hong Guo
Keyword(s):  
Real Time ◽  
Expressive Power ◽  
Process Models ◽  
Software Systems ◽  
Real Time System ◽  
Code Generator ◽  
Automatic Teller Machine ◽  
Allocation Process ◽  
Design Paradigm ◽  
Formal Design

An Automated Teller Machine (ATM) is a safety-critical and real-time system that is highly complicated in design and implementation. This article presents the formal design, specification, and modeling of the ATM system using a denotational mathematics known as Real-Time Process Algebra (RTPA). The conceptual model of the ATM system is introduced as the initial requirements for the system. The architectural model of the ATM system is created using RTPA architectural modeling methodologies and refined by a set of Unified Data Models (UDMs), which share a generic mathematical model of tuples. The static behaviors of the ATM system are specified and refined by a set of Unified Process Models (UPMs) for the ATM transition processing and system supporting processes. The dynamic behaviors of the ATM system are specified and refined by process priority allocation, process deployment, and process dispatch models. Based on the formal design models of the ATM system, code can be automatically generated using the RTPA Code Generator (RTPA-CG), or be seamlessly transformed into programs by programmers. The formal models of ATM may not only serve as a formal design paradigm of real-time software systems, but also a test bench for the expressive power and modeling capability of exiting formal methods in software engineering.

The Formal Design Model of an Automatic Teller Machine (ATM)

2012 ◽  
pp. 263-287 ◽  
Author(s):  
Yingxu Wang ◽  
Yanan Zhang ◽  
Philip C.-Y. Sheu ◽  
Xuhui Li ◽  
Hong Guo
Keyword(s):  
Real Time ◽  
Expressive Power ◽  
Process Models ◽  
Software Systems ◽  
Real Time System ◽  
Code Generator ◽  
Allocation Process ◽  
Design Paradigm ◽  
Process Deployment ◽  
Formal Design

An Automated Teller Machine (ATM) is a safety-critical and real-time system that is highly complicated in design and implementation. This paper presents the formal design, specification, and modeling of the ATM system using a denotational mathematics known as Real-Time Process Algebra (RTPA). The conceptual model of the ATM system is introduced as the initial requirements for the system. The architectural model of the ATM system is created using RTPA architectural modeling methodologies and refined by a set of Unified Data Models (UDMs), which share a generic mathematical model of tuples. The static behaviors of the ATM system are specified and refined by a set of Unified Process Models (UPMs) for the ATM transition processing and system supporting processes. The dynamic behaviors of the ATM system are specified and refined by process priority allocation, process deployment, and process dispatch models. Based on the formal design models of the ATM system, code can be automatically generated using the RTPA Code Generator (RTPA-CG), or be seamlessly transformed into programs by programmers. The formal models of ATM may not only serve as a formal design paradigm of real-time software systems, but also a test bench for the expressive power and modeling capability of exiting formal methods in software engineering.

Sign in / Sign up

Export Citation Format

Share Document