Model-Driven Design and ASM-Based Validation of Embedded Systems

2010 ◽  
pp. 24-54 ◽  
Author(s):  
Angelo Gargantini ◽  
Elvinia Riccobene ◽  
Patrizia Scandurra
Keyword(s):  
Embedded System ◽  
Graphical Models ◽  
Code Generation ◽  
Formal Method ◽  
System Level ◽  
Levels Of Abstraction ◽  
Model Driven ◽  
The Embedded System ◽  
On Chip ◽  
High Level

In the embedded system and System-on-Chip (SoC) design area, the increasing technological complexity coupled with requests for more performance and shorter time to market have caused a high interest for new methods, languages and tools capable of operating at higher levels of abstraction than the conventional system level. This chapter presents a model-driven and tool-assisted development process of SoCs, which is based on high-level UML design of system components, guarantees SystemC code generation from graphical models, and allows validation of system behaviors on formal models automatically derived from UML models. An environment for system design and analysis is also presented, which is based on a UML profile for SystemC and the Abstract State Machine formal method.

scholarly journals Compositional Verification of Security Properties for Embedded Execution Platforms

10.29007/h4rv ◽  
2018 ◽  
Author(s):  
Christoph Baumann ◽  
Oliver Schwarz ◽  
Mads Dam
Keyword(s):  
Embedded System ◽  
Message Passing ◽  
Theorem Prover ◽  
System Level ◽  
Compositional Verification ◽  
System Specification ◽  
Security Proof ◽  
Security Properties ◽  
On Chip ◽  
High Level

The security of embedded systems can be dramatically improved through the use of formally verified isolation mechanisms such as separation kernels, hypervisors, or microkernels. For trustworthiness, particularly for system level behaviour, the verifications need precise models of the underlying hardware. Such models are hard to attain, highly complex, and proofs of their security properties may not easily apply to similar but different platforms. This may render verification economically infeasible.To address these issues, we propose a compositional top-down approach to embedded system specification and verification, where the system-on-chip is modeled as a network of distributed automata communicating via paired synchronous message passing. Using abstract specifications for each component allows to delay the development of detailed models for cores, devices, etc., while still being able to verify high level security properties like integrity and confidentiality, and soundly refine the result for different instantiations of the abstract components at a later stage.As a case study, we apply this methodology to the verification of information flow security for an industry scale security-oriented hypervisor on the ARMv8-A platform. The hypervisor statically assigns (multiple) cores to each guest system and implements a rudimentary, but usable, inter guest communication discipline. We have completed a pen-and-paper security proof for the hypervisor down to state transition level and report on a partially completed verification of guest mode security in the HOL4 theorem prover.

scholarly journals Model-Driven Architectural Framework towards Safe and Secure Nuclear Power Reactors

Sensors ◽  
2021 ◽  
Vol 21 (15) ◽  
pp. 5136
Author(s):  
Bassem Ouni ◽  
Christophe Aussagues ◽  
Saadia Dhouib ◽  
Chokri Mraidha
Keyword(s):  
Nuclear Power ◽  
Nuclear Reactors ◽  
System Development ◽  
Levels Of Abstraction ◽  
Model Driven ◽  
Case System ◽  
Architectural Framework ◽  
Performance Check ◽  
High Level ◽  
Different Levels

Sensor-based digital systems for Instrumentation and Control (I&C) of nuclear reactors are quite complex in terms of architecture and functionalities. A high-level framework is highly required to pre-evaluate the system’s performance, check the consistency between different levels of abstraction and address the concerns of various stakeholders. In this work, we integrate the development process of I&C systems and the involvement of stakeholders within a model-driven methodology. The proposed approach introduces a new architectural framework that defines various concepts, allowing system implementations and encompassing different development phases, all actors, and system concerns. In addition, we define a new I&C Modeling Language (ICML) and a set of methodological rules needed to build different architectural framework views. To illustrate this methodology, we extend the specific use of an open-source system engineering tool, named Eclipse Papyrus, to carry out many automation and verification steps at different levels of abstraction. The architectural framework modeling capabilities will be validated using a realistic use case system for the protection of nuclear reactors. The proposed framework is able to reduce the overall system development cost by improving links between different specification tasks and providing a high abstraction level of system components.

A Novel Embedded System Architecture for Fire Detection Based on Image Processing

2014 ◽  
Vol 608-609 ◽  
pp. 454-458
Author(s):  
Wei Bai ◽  
Chen Yuan Hu
Keyword(s):  
Image Processing ◽  
Embedded System ◽  
System Architecture ◽  
Cooperative Control ◽  
Processing System ◽  
Fire Detection ◽  
System Level ◽  
High Definition ◽  
The Embedded System ◽  
Pass Through

This paper presents novel logic/software co-work architecture for embedded high definition image processing platform, which is built by the considerations of system level, board hardware level, and the tasks partition between CPU processing and programmable logic based on the latest launched System on Chip Field Programmable Gate Array (Soc FPGA) – Xilinx ZC7020. For this case, we comprehensive analyze of the critical data paths: the uniform Advanced Extensible Interface (AXI) processing between processing system (PS) and processing logic (PL), including high definition video pass through PL to PS and PS software processing send to PL for speed up. We have included the transplant of opensource Linux, multiprocessing cooperative control and boot loader in PS side. Since the general platform is proposed, a fire detection approach based on high definition image processing is implemented. Experiment results indicated the feasibility and universality of the embedded system architecture.

scholarly journals Area Optimization using Structural Modeling for Gate Level Implementation of SPI for Microcontroller

2019 ◽  
Vol 9 (1) ◽  
pp. 4763-4768
Keyword(s):  
Embedded System ◽  
Optimization Techniques ◽  
Consumer Electronics ◽  
Full Potential ◽  
Disruptive Technologies ◽  
Serial Peripheral Interface ◽  
Area Optimization ◽  
The Embedded System ◽  
On Chip ◽  
Design And Testing

The need for miniaturization has been the driving force in chip manufacturing. The proliferation of IoT, robotics, consumer electronics and medical instruments pose unprecedented demands on the embedded system design. The area optimization can be achieved either by reducing the size of transistors or by optimizing (reducing) the circuit at the gate level. The first solution has attracted many researchers while the later has not been explored to its full potential. The aim is to design a System on Chip (SoC) to satisfy the dynamic requirements of disruptive technologies while occupying the lesser area. The design and testing of communication interfaces such as Serial Peripheral Interface (SPI), Inter-IC Communication (I2C), Universal Asynchronous Receiver and Transmitter (UART) are very crucial in the area optimization of microcontroller design. Since SPI being an important communication protocol, this work reports the preliminary research carried in the design and verification of it. In this work, Verilog is used for the design and verification of the SPI module. The results show that there is a drastic reduction in the number of Look-Up-Tables (LUTs) and slices required to build the circuit. We conclude that sophisticated optimization techniques of the circuit at the gate level has the potential to reduce the area by half.

scholarly journals Adaptivity in high-performance embedded systems: a reactive control model for reliable and flexible design

2014 ◽  
Vol 29 (4) ◽  
pp. 433-451
Author(s):  
Huafeng Yu ◽  
Abdoulaye Gamatié ◽  
Éric Rutten ◽  
Jean-Luc Dekeyser
Keyword(s):  
Embedded Systems ◽  
Embedded System ◽  
Code Generation ◽  
High Performance ◽  
Control Model ◽  
Multimedia System ◽  
Reactive Control ◽  
Data Intensive ◽  
On Chip ◽  
Automatic Code

AbstractSystem adaptivity is increasingly demanded in high-performance embedded systems, particularly in multimedia system-on-chip (SoC), owing to growing quality-of-service requirements. This paper presents a reactive control model that has been introduced in Gaspard, our framework dedicated to SoC hardware/software co-design. This model aims at expressing adaptivity as well as reconfigurability in systems performing data-intensive computations. It is generic enough to be used for description in the different parts of an embedded system, for example, specification of how different data-intensive algorithms can be chosen according to some computation modes at the functional level; and expression of how hardware components can be selected via the usage of a library of intellectual properties according to execution performances. The transformation of this model toward synchronous languages is also presented, in order to allow an automatic code generation usable for formal verification, based on techniques such as model checking and controller synthesis, as illustrated in the paper. This work, based on Model-Driven Engineering and the standard UML MARTE profile, has been implemented in Gaspard.

scholarly journals Model Driven Engineering for MPSoC Design Space Exploration

2008 ◽  
Vol 3 (1) ◽  
pp. 13-22
Author(s):  
Marcio F. da S. Oliveira ◽  
Eduardo W. Brião ◽  
Francisco A. Nascimento ◽  
Flávio R. Wagner
Keyword(s):  
Code Generation ◽  
Design Space Exploration ◽  
Design Space ◽  
Space Exploration ◽  
Design Stage ◽  
Model Driven Engineering ◽  
Early Design Stage ◽  
Model Driven ◽  
Design Activities ◽  
High Level

This paper presents a Model Driven Engineering approach for MPSoC Design Space Exploration (DSE) to deal with the ever-growing challenge of designing complex embedded systems. This approach allows the designer to automatically select the most adequate modeling solution for application, platform, and mapping between application and platform, in an integrated and simultaneous way and at a very early design stage, before system synthesis and code generation have been performed. The exploration is based on high-level estimates of physical characteristics of each candidate solution. In an experimental setting, the DSE tool automatically performs four design activities: it selects the number of processors, maps tasks to processors, allocates processors to bus segments, and sets the voltage of each processor. Experimental results, extracted from a DSE scenario for a real application, show that the proposed estimation and exploration approach may find a suitable solution regarding the design requirements and constraints in a very short time, with an acceptable accuracy, without relying on costly synthesis-and-simulation cycles.

Concern Separation for Adaptive QoS Modeling in Distrbuted Real-Time Embedded Systems

2010 ◽  
pp. 85-113 ◽  
Author(s):  
Jeff Gray ◽  
Sandeep Neema ◽  
Jing Zhang ◽  
Yuehua Lin ◽  
Ted Bapty ◽  
...  
Keyword(s):  
Real Time ◽  
Graphical Models ◽  
Model Transformations ◽  
Modeling Language ◽  
Model Driven ◽  
Trade Offs ◽  
Design Alternatives ◽  
Domain Specific Modeling ◽  
High Level ◽  
Qos Adaptation

The development of distributed real-time and embedded (DRE) systems is often challenging due to conflicting quality-of-service (QoS) constraints that must be explored as trade-offs among a series of alternative design decisions. The ability to model a set of possible design alternatives—and to analyze and simulate the execution of the representative model—helps derive the correct set of QoS parameters needed to satisfy DRE system requirements. QoS adaptation is accomplished via rules that specify how to modify application or middleware behavior in response to changes in resource availability. This chapter presents a model-driven approach for generating QoS adaptation rules in DRE systems. This approach creates high-level graphical models representing QoS adaptation policies. The models are constructed using a domain-specific modeling language—the adaptive quality modeling language (AQML)—which assists in separating common concerns of a DRE system via different modeling views. The chapter motivates the need for model transformations to address crosscutting and scalability concerns within models. In addition, a case study is presented based on bandwidth adaptation in video streaming of unmanned aerial vehicles.

Model-Based Development

2011 ◽  
pp. 289-312 ◽  
Author(s):  
Juan D. Lara ◽  
Esther Guerra ◽  
Hans Vangheluwe
Keyword(s):  
Programming Languages ◽  
Graphical Models ◽  
Code Generation ◽  
Simulation Analysis ◽  
Model Simulation ◽  
General Purpose ◽  
Test Case ◽  
Model Driven ◽  
Model Based ◽  
Design Activities

Since the beginning of computer science more than 50 years ago, software engineers have sought techniques resulting in higher levels of quality and productivity. Some of these efforts have concentrated in increasing the level of abstraction in programming languages (from assembler to structured languages to object-oriented languages). In the last few years, we have witnessed an increasing focus on development based on high-level, graphical models. They are used not only as a means to documentthe analysis and design activities, but also as the actual “implementation” of the application, as well as for automatic analysis, code, and test case generation. The notations used to describe the models can be standard and general purpose (for example, UML) or tightly customized for the application domain. Code generation for the full application is only accomplished for specific, well-understood application domains. A key initiative in this direction is OMG’s Model-Driven Architecture (MDA), where models are progressively transformed until executable code is obtained. In this chapter, we give an overview of these technologies and propose ideas following this line (concerning metamodeling and the use of visual languages for the specification of model transformation, model simulation, analysis and code generation), and examine the impact of model-based techniques in the development process.

System-Level Design of NoC-Based Dependable Embedded Systems

2014 ◽  
pp. 478-512
Author(s):  
Mihkel Tagel ◽  
Peeter Ellervee ◽  
Gert Jervan
Keyword(s):  
Design Space Exploration ◽  
System Level ◽  
System Level Design ◽  
Levels Of Abstraction ◽  
Technology Scaling ◽  
Communication Problems ◽  
Systems On Chip ◽  
Level Design ◽  
On Chip ◽  
Manufacturing Yield

Technology scaling into subnanometer range will have impact on the manufacturing yield and quality. At the same time, complexity and communication requirements of systems-on-chip (SoC) are increasing, thus making a SoC designer goal to design a fault-free system a very difficult task. Network-on-chip (NoC) has been proposed as one of the alternatives to solve some of the on-chip communication problems and to address dependability at various levels of abstraction. This chapter concentrates on system-level design issues of NoC-based systems. It describes various methods proposed for NoC architecture analysis and optimization, and gives an overview of different system-level fault tolerance methods. Finally, the chapter presents a system-level design framework for performing design space exploration for dependable NoC-based systems.

Sign in / Sign up

Export Citation Format

Share Document