Specification-correct and scalable coordination of Grid applications

The so called “invisible Grid”, transparent to application developers, is still far from being a reality. One reason is that the workflow model, which emerged as a widely accepted paradigm for high-level composition of Grid applications, is based on a low-level imperative programming model prone to programming errors. The issue of developing correct (bug-free) Grid applications has not been addressed by the community.We propose a new model for building Grid applications based on two programming phases: (1) formal functional specification, written by the application developer not interested in any Grid-related issues; (2) imperative workflow-based coordination, written by the computer scientist, which ports and efficiently executes the specification onto the Grid. A correctness checker automatically connects both parts at compile-time and insures the correct execution of the workflow coordination with respect to the formal specification.We validate our approach for three scientific applications and show real-world experimental results that demonstrate the scalability of our coordination model and the fact that the overhead introduced by our correctness checker is insignificant when compared to the latencies exhibited by the Grid middleware software.