Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

## Developing portable embedded software for multicore systems through formal abstraction and refinement

• Author(s):
• DOI:

$16.00 (plus tax if applicable) ##### Buy Knowledge Pack 10 chapters for$120.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Name:*
Email:*
Name:*
Email:*
Department:*
Why are you recommending this title?
Select reason:

Many-Core Computing: Hardware and Software — Recommend this title to your library

## Thank you

Run-time management (RTM) systems are used in embedded systems to dynamically adapt hardware performance to minimise energy consumption. An RTM system implementation is coupled with the hardware platform specifications and is implemented individually for each specific platform. A significant challenge is that RTM software can require laborious manual adjustment across different hardware platforms due to the diversity of architecture characteristics. Hardware specifications vary from one platform to another and include a number of characteristic such as the number of supported voltage and frequency (VF) settings. Formal modelling offers the potential to simplify the management of platform diversity by shifting the focus away from handwritten platform-specific code to platform-independent models from which platform-specific implementations are automatically generated. The article presents an overview of the motivations for this work. It goes on to overview the RTM architecture and requirements and introduce the Event-B formal method and its tool support. The article then describes the Event-B model of two different RTMs and presents the portability support provided by formal modelling and code generation. Finalyy, it reviews the verification and experimental results.

Chapter Contents:

• 14.1 Introduction
• 14.2 Motivation
• 14.2.1 From identical formal abstraction to specific refinements
• 14.2.2 From platform-independent formal model to platform-specific implementations
• 14.3 RTM cross-layer architecture overview
• 14.4 Event-B
• 14.4.1 Structure and notation
• 14.4.1.1 Context structure
• 14.4.1.2 Machine structure
• 14.4.2 Refinement
• 14.4.3 Proof obligations
• 14.4.4 Rodin: event-B tool support
• 14.5 From identical formal abstraction to specific refinements
• 14.5.1 Abstraction
• 14.5.2 Learning-based RTM refinements
• 14.5.3 Static decision-based RTM refinements
• 14.6 Code generation and portability support
• 14.7 Validation
• 14.8 Conclusion and future directions
• References

Preview this chapter:

Developing portable embedded software for multicore systems through formal abstraction and refinement, Page 1 of 2

| /docserver/preview/fulltext/books/pc/pbpc022e/PBPC022E_ch14-1.gif /docserver/preview/fulltext/books/pc/pbpc022e/PBPC022E_ch14-2.gif

### Related content

content/books/10.1049/pbpc022e_ch14
pub_keyword,iet_inspecKeyword,pub_concept
6
6
This is a required field