Towards a Formal Foundation for Aggregating Scientific Workflows

In e-Science, scientific workflow systems are used to share data and knowledge in collaborative experiments. In recent work we discussed the concepts of a workflow bus [1], allowing multiple workflow systems to be coupled in a meta-workflow system with multiple execution models. In this paper we propose an approach for a formal model to perform the task of reasoning of about the execution models of such workflow systems. We propose that I/O Automata can be used as a formalism to prove the correctness of complicated workflows involving multiple workflow engines and execution models.