Validating Timing And Scheduling Mar-te‟s Profils Using Event B: Case Study Of A Gpu Architecture

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.