Formal Approach For Gpu Architecture Schedulability

Parallel application modelling and specifying is not an easy task to do because it treats tasks scheduling and time evolution. Graphics processing Unit is one of the main architectures that guaranties parallel execution. Event B is a skilled formal language based on sets theories. Our goal is to model and to specify the parallel execution of programs on GPU using Event B & RODIN platform. We are interesting to timing and scheduling of tasks on GPU.