Embedded System Verification Using Formal Model an Approach Based on the Combined Use of UML and Maude Language

2018 ◽  
Vol 6 (2) ◽  
pp. 42-58
Author(s):  
Meliouh Amel ◽  
Chaoui Allaoua
Keyword(s):  
Embedded System ◽  
Real Time ◽  
Code Generation ◽  
Formal Model ◽  
System Modeling ◽  
Automatic Generation ◽  
Modeling Tools ◽  
Automated Modeling ◽  
Combined Use ◽  
System Verification

The approach proposed in this article presents a formal verification of embedded systems. The method relies on an automated modeling and code generation based on the systems' behavior. The key concept is the combined use of a subset of UML behavior diagrams extended with timing annotations (Real-Time Statechart and Real-Time Collaboration diagrams) for system modeling and the Maude language for verification. First, UML modeling tools are developed. Then, an automatic generation of equivalent Maude specification is performed. The approach is based on code generation. This is why it is possible to use an available model checking tool to verify certain timed properties represented in Linear Temporal Logic (LTL). The meta-modeling tool ATOM3 is used. A case study is presented to illustrate the feasibility of the approach.

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.

An Operational Semantics of Real-Time Process Algebra (RTPA)

2011 ◽  
pp. 218-238
Author(s):  
Yingxu Wang ◽  
Cyprian F. Ngolah
Keyword(s):  
Real Time ◽  
Code Generation ◽  
Intelligent Systems ◽  
Process Algebra ◽  
System Modeling ◽  
Operational Semantics ◽  
Software Systems ◽  
Time Process ◽  
Modeling Methodology ◽  
Reduction Machine

The need for new forms of mathematics to express software engineering concepts and entities has been widely recognized. Real-time process algebra (RTPA) is a denotational mathematical structure and a system modeling methodology for describing the architectures and behaviors of real-time and nonrealtime software systems. This article presents an operational semantics of RTPA, which explains how syntactic constructs in RTPA can be reduced to values on an abstract reduction machine. The operational semantics of RTPA provides a comprehensive paradigm of formal semantics that establishes an entire set of operational semantic rules of software. RTPA has been successfully applied in real-world system modeling and code generation for software systems, human cognitive processes, and intelligent systems.

An Operational Semantics of Real-Time Process Algebra (RTPA)

2009 ◽  
pp. 3340-3360
Author(s):  
Yingxu Wang ◽  
Cyprian F. Ngolah
Keyword(s):  
Real Time ◽  
Code Generation ◽  
Intelligent Systems ◽  
Process Algebra ◽  
System Modeling ◽  
Operational Semantics ◽  
Software Systems ◽  
Time Process ◽  
Modeling Methodology ◽  
Reduction Machine

The need for new forms of mathematics to express software engineering concepts and entities has been widely recognized. Real-time process algebra (RTPA) is a denotational mathematical structure and a system modeling methodology for describing the architectures and behaviors of real-time and nonreal-time software systems. This article presents an operational semantics of RTPA, which explains how syntactic constructs in RTPA can be reduced to values on an abstract reduction machine. The operational semantics of RTPA provides a comprehensive paradigm of formal semantics that establishes an entire set of operational semantic rules of software. RTPA has been successfully applied in real-world system modeling and code generation for software systems, human cognitive processes, and intelligent systems.

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.

Embedded System Design Using Formal Model Refinement: An Approach Based on the Combined Use of UML and the B Language

2004 ◽  
Vol 9 (2) ◽  
pp. 67-99 ◽  
Author(s):  
Nikolaos S. Voros ◽  
Colin F. Snook ◽  
Stefan Hallerstede ◽  
Konstantinos Masselos
Keyword(s):  
Embedded System ◽  
System Design ◽  
Formal Model ◽  
Model Refinement ◽  
Embedded System Design ◽  
Combined Use
Sign in / Sign up

Export Citation Format

Share Document