Models & Optimisation and Mathematical Analysis Journal
Volume 2, Numéro 2, Pages 30-43
2012-12-25
Validating Timing And Scheduling Mar-te‟s Profils Using Event B: Case Study Of A Gpu Architecture
Authors : Zouaneb Imane . Belarbi Mostefa . Chouarfia Abdellah .
Abstract
promoted filed to parallelize application thanks to the multi-core GPU architecture. GPUs (Graphic Processing Unit) ensure the parallelism on the chip and discharge the Central Processing Unit (CPU). The specification of scheduling and timing on GPUs had been always a research problematic. MARTE is an efficient semi formal tool for specifica-tion thanks to the several diagrams of UML and the new profiles provided by MARTE which treats the software, hardware and scheduling of the specified SoC. But it still none valid specification because it isn’t proved. That’s why we propose to couple MARTE with the formal method Event B to have a valid and proved specification and to validate the task schedul-ing on the GPU. After having a valid specification a second phase of executable code generation from Event B specification is essential to execute parallel applica-tions on the GPU. CUDA is an efficient programming language on GPUs because it offers new tools for parallel programming.
Keywords
GPU, MARTE, Scheduling, Timing Event B, Re-finements, Code generation, CUDA.
Les articles similaires
Aitzai Abdelhakim
.
Dabah Adel
.
Boudhar Mourad
.
pages 949-961.
Zouaneb Imane
.
Belarbi Mostefa
.
Chouarfia Abdellah
.
pages 10-16.
كرور زهير
.
ص 268-284.
أستاذ مساعد ابراهيم محمد عوده ابو اعمر
.
pages 403-426.
