Formal Modelling and Verification of Grid Systems

Grid systems is the leading infrastructure for computing intensive software. Such systems is used in different application domains, e.g. from simulating how the universe evolved just after the big bang to support services that influence our daily life such as precise calculation of the weather forecast. Researchers at the Bergen University College has in the period October 2009 to August 2014 performed research on how to improve Grid technologies for the future in the FORMGRID project. The main objective of the FORMGRID project is to develop new techniques and software tools for diagrammatically modelling grid computing systems, and for formally verifying their correct behaviour. Grid computing systems are networks of loosely coupled computers which can be used together as a "virtual" computer for solving problems which are computationally hard and/or require very large storage capacity. The FORMGRID project has developed techniques and tools that could be applied for designing and analysing grid computing systems. One of the key results of the project is that the developed tools will allow users to model systems by constructing graphical diagrams, following the model-driven engineering philosophy, and formally verify the correctness of the system in a automatic manner. During the project it's created new technologies to easier translate grid software between different architectures, allowing more efficient use of the grid computing facilities. It has been written two Ph.D. thesis's connected to the FORMGRID project. The Ph.D candidate Florian Mantz has conducted research on how to adapt system according to changes in requirements and underlying modelling formalisms he has written a Ph.D. thesis on "Coupled Transformations of Graph Structures applied to Model Migration". The Ph.D candidate Piotr Kazmierczak has studied how interconnected systems can be modelled with use of software agents that respect social laws, he has written a Ph.D. thesis on "Agents That Play By the Rules, On using Social Laws as a coordination Mechanism for Multiagent Systems".

The aim of the FORMGRID project is to develop new techniques and tools for designing and analysing grid computing systems. The project is *timely*, because it develops technologies which can be applied to problems of ultimately high societal importance fo r which current methods are insufficient. The research is *novel*, because it combines the existing areas of diagrammatic modelling and model-driven development on the one hand and formal model checking on the other, in a new way. The project is *strategi cally important*, since it forms a part of HiB's new strategic research programme in the area of software for distributed systems and develops generic technology which will lay the foundations for future research projects and collaborations with industry and academia. The project is *realistic*, since it comprises several of HiB's scientific competence areas and involves collaboration with leading international groups. The research is organised in four interdependent work packages: (1) Development of a formal framework for diagrammatic models of grid systems (2) Development of a model checking framework emplying diagrammatic models (3) Implementation of software tools (4) Case studies