Your browser does not support JavaScript!

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

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

For access to this article, please select a purchase option:

Buy chapter PDF
(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.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Your details
Why are you recommending this title?
Select reason:
Many-Core Computing: Hardware and Software — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

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
  • Context structure
  • 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

Inspec keywords: distributed programming; software portability; embedded systems; multiprocessing systems; formal verification; specification languages

Other keywords: energy consumption; platform-independent models; voltage and frequency settings; formal refinement; multicore systems; platform specifications; Event-B formal method; formal modelling; RTM software; embedded systems; hardware performance; formal abstraction; code generation; RTM system implementation; run-time management systems; portable embedded software

Subjects: Formal methods; Distributed systems software; High level languages; Multiprocessing systems

Preview this chapter:
Zoom in

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

This is a required field
Please enter a valid email address