Modeling and Formal Validation of High-Performance Embedded Systems

Author

Gamatie, Abdoulaye ; Rutten, Éric ; Yu, Huafeng ; Boulet, Pierre ; Dekeyser, Jean-Luc

Author_Institution

LIFL, Univ. de Lille 1, Villeneuve-d´´Ascq, France

fYear

2008

fDate

1-5 July 2008

Firstpage

215

Lastpage

222

Abstract

This paper presents an approach for the modeling and formal validation of high-performance systems. The approach relies on the repetitive model of computation used to express the parallelism of such systems within the Gaspard framework, which is dedicated to the codesign of high-performance system-on-chip. The system descriptions obtained with this model are then projected on the synchronous model of computation. The result of this projection consists of an equational model that allows one to formally analyze clock synchronizability issues so as to guarantee the reliable deployment of systems on platforms.

Keywords

clocks; embedded systems; system-on-chip; Gaspard framework; clock synchronizability; equational model; formal validation; formally analysis; high-performance embedded systems; high-performance system-on-chip; modeling; CMOS image sensors; Clocks; Computational modeling; Computer displays; Embedded system; Equations; Hardware; Synchronization; System-on-a-chip; Thin film transistors;

fLanguage

English

Publisher

ieee

Conference_Titel

Parallel and Distributed Computing, 2008. ISPDC '08. International Symposium on

Conference_Location

Krakow

Print_ISBN

978-0-7695-3472-5

Type

conf

DOI

10.1109/ISPDC.2008.28

Filename

4724249