The Event-B Modelling with Operators-based Refinement of NoC-based Wireless Sensors Networks

2017 ◽  
Author(s):  
Abdelhamid Hariche ◽  
Mostefa Belarbi ◽  
Abdallah Chouarfia ◽  
Abdelkader Chaib
Keyword(s):  
Embedded System ◽  
Code Generation ◽  
Wireless Sensors ◽  
High Performance ◽  
Formal Method ◽  
Abstract Data Type ◽  
Generation Process ◽  
Critical Systems ◽  
Colored Graph ◽  
Abstract Data

The need for high performance, available and reliable embedded systems has made computing systems increasingly complex. Formal methods have the ability to produce critical systems for large industrial projects, and this by creating an original mathematical model that can be formally refined in levels until the final refinement which contains enough of details for an implementation. This work is a first step of VHDL code generation process, it represents how to elaborate formally an embedded system using Abstract data type in a form of theories (NoC, WNoC, colored graph, VHDL) and how to ensure in systematic way all the details and complexity of this system using operators of refinement (Create, Rename, Restrict, Enrich)that are recently proposed for the Event-B method. All the theories are deployed, discharged and used in Event-B models to represent and enhance the performance of this self-organization reliability solution for the wireless sensors network of NoC-based system. This paper summerize the fruit of using new proposed approach for the Event-B formal method that persist the NoC-based ditributed system instead of consuming more than 70% of realization time with any analytic method.

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.

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 Testing embedded systems using test cases generated through combinatorial techniques

2018 ◽  
Vol 7 (2.7) ◽  
pp. 146
Author(s):  
Lakshmi Prasad Mudarakola ◽  
J K.R. Sastry ◽  
V Chandra Prakash
Keyword(s):  
Embedded Systems ◽  
Embedded System ◽  
Traffic Control ◽  
Nuclear Reactor ◽  
Test Cases ◽  
Critical Systems ◽  
Daily Lives ◽  
Intelligent Devices ◽  
Wireless Infrastructure ◽  
Combinatorial Methods

Thorough testing of embedded systems is required especially when the systems are related to monitoring and controlling the mission critical and safety critical systems. The embedded systems must be tested comprehensively which include testing hardware, software and both together. Embedded systems are highly intelligent devices that are infiltrating our daily lives such as the mobile in your pocket, and wireless infrastructure behind it, routers, home theatre system, the air traffic control station etc. Software now makes up 90% of the value of these devices. In this paper, authors present different methods to test an embedded system using test cases generated through combinatorial techniques. The experimental results for testing a TMCNRS (Temperature Monitoring and Controlling Nuclear Reactor System) using test cases generated from combinatorial methods are also shown.

scholarly journals Towards Analysis-Driven Scientific Software Architecture: The Case for Abstract Data Type Calculus

2008 ◽  
Vol 16 (4) ◽  
pp. 329-339 ◽  
Author(s):  
Damian W.I. Rouson
Keyword(s):  
Software Architecture ◽  
Search Strategy ◽  
Object Oriented ◽  
New Physics ◽  
Data Type ◽  
Abstract Data Type ◽  
Scientific Software ◽  
Code Size ◽  
Design Metrics ◽  
Abstract Data

This article approaches scientific software architecture from three analytical paths. Each path examines discrete time advancement of multiphysics phenomena governed by coupled differential equations. The new object-oriented Fortran 2003 constructs provide a formal syntax for an abstract data type (ADT) calculus. The first analysis uses traditional object-oriented software design metrics to demonstrate the high cohesion and low coupling associated with the calculus. A second analysis from the viewpoint of computational complexity theory demonstrates that a more representative bug search strategy than that considered by Rouson et al. (ACM Trans. Math. Soft.34(1) (2008)) reduces the number of lines searched in a code with λ total lines from O(λ2) to O(λ log2λ ), which in turn becomes nearly independent of the overall code size in the context of ADT calculus. The third analysis derives from information theory an argument that ADT calculus simplifies developer communications in part by minimizing the growth in interface information content as developers add new physics to a multiphysics package.

scholarly journals Hardware-Assisted Security Monitoring Unit for Real-Time Ensuring Secure Instruction Execution and Data Processing in Embedded Systems

Micromachines ◽  
2021 ◽  
Vol 12 (12) ◽  
pp. 1450
Author(s):  
Xiang Wang ◽  
Zhun Zhang ◽  
Qiang Hao ◽  
Dongdong Xu ◽  
Jiqing Wang ◽  
...  
Keyword(s):  
Embedded Systems ◽  
Data Processing ◽  
Embedded System ◽  
High Performance ◽  
Program Execution ◽  
Security Monitoring ◽  
Railway Systems ◽  
On Chip ◽  
Capability Evaluation ◽  
Security Capability

The hardware security of embedded systems is raising more and more concerns in numerous safety-critical applications, such as in the automotive, aerospace, avionic, and railway systems. Embedded systems are gaining popularity in these safety-sensitive sectors with high performance, low power, and great reliability, which are ideal control platforms for executing instruction operation and data processing. However, modern embedded systems are still exposing many potential hardware vulnerabilities to malicious attacks, including software-level and hardware-level attacks; these can cause program execution failure and confidential data leakage. For this reason, this paper presents a novel embedded system by integrating a hardware-assisted security monitoring unit (SMU), for achieving a reinforced system-on-chip (SoC) on ensuring program execution and data processing security. This architecture design was implemented and evaluated on a Xilinx Virtex-5 FPGA development board. Based on the evaluation of the SMU hardware implementation in terms of performance overhead, security capability, and resource consumption, the experimental results indicate that the SMU does not lead to a significant speed degradation to processor while executing different benchmarks, and its average performance overhead reduces to 2.18% on typical 8-KB I/D-Caches. Security capability evaluation confirms the monitoring effectiveness of SMU against both instruction and data tampering attacks. Meanwhile, the SoC satisfies a good balance between high-security and resource overhead.

scholarly journals Design and Implementation ofReal-time Electrical Stimulation Artifact Suppression based on STM32

2021 ◽  
Vol 12 (5) ◽  
pp. 424-427
Author(s):  
Sangsoo Park, Hojun Yeom
Keyword(s):  
Central Nervous System ◽  
Nervous System ◽  
Electrical Stimulation ◽  
Embedded System ◽  
Muscle Contraction ◽  
Real Time ◽  
High Performance ◽  
Floating Point ◽  
Time Signal ◽  
Central Nervous System Damage

A biosignal is used as a control signal for electrical stimulation to restore weakened muscle function due to damage to the central nervous system. In patients with central nervous system damage, sufficient muscle contraction does not occur spontaneously. In this case, applying electrical stimulation can cause normal muscle contraction. However, it is necessary to remove the electrical stimulation artifact caused by the electrical stimulation. This paper describes a system design that removes electrical stimulation artifact in real time using a Cortex-M4-based STM32F processor. The STM32F is a very advantageous MCU for such DSPs, especially because it has a built-in floating point operator. Using STM32F's various high-performance peripherals (12-bit parallel ADC and 12-bit DAC, UART, Timer), an optimized embedded system was implemented.In this paper, the simulated and real-time results were compared and evaluated with the designed fir filter. In addition, the performance of the filter was evaluated through frequency analysis. As a result, it was verified that a high-performance 32-bit STM32F with floating point calculator and various peripherals is suitable for real-time signal processing

Sign in / Sign up

Export Citation Format

Share Document