Formal modelling of a coordination system:: From practice to theory, and back again

In this work, we report an experience that illustrates the interplay between formal methods and real software development. Starting from a Web-enable Coordination Service (WCS) based on JavaSpaces technology which had been successfully used in an industrial project, we built a formal model for the system in order to study its properties; specifically, our aim was to prove that Linda semantics was preserved in several layers of complex mappings from XML documents to Java objects. Once this objective was achieved (at least in a simplified, idealistic version), we observed several possibilities of extending the coordination system at the model level. In particular, we identified that it was possible to enhance the formal model with transactional capabilities, taking advantage of the similarity of our model to rule-based systems. At present, we are working on the translation of this theoretical result to practice, in order to improve our Web Coordination Service.