Formal Modelling and Verification of Grid Systems

Gridsystemer er den viktigste infrastrukturen for beregningsintensiv programvare. De har flere forskjellige praktiske anvendelser f.eks. blir de brukt til til å simulere universets utvikling i tiden rett etter big bang. De blir også brukt i mer dagligdagse anvendelser som for eksempel presis beregning av værmeldinger. Forskere ved høgskolen i Bergen har i perioden oktober 2009 til august 2014 gjenomført FORMGRID prosjektet hvor de har forsket på hvordan en kan forbedre fremtidens grid teknologier. Hovedmålet med FORMGRID prosjektet er å utvikle nye teknikker og programvareverktøy for diagrammatisk modellering av grid systemer samt teknikker for å verifisere at systemene har korekt oppførsel. Grid systemer er nettverk av løst koplede datamaskiner som kan benyttes som en virtuell supercomputer for å løse beregningsintensive problemer og/eller krever ekstremt stor lagringskapasitet. FORMGRID prosjektet har utviklet teknikker og verktøy som kan anvendes til design og analyse av grid systemer. Et av de viktigste resultatene i prosjektet er at ved å følge en modellbasert utviklingsstrategi kan brukere modellere systemer ved å konstruere grafiske modeller (diagram) og en har automatisert en prosedyre for å formelt verifisere at systemene er korekte. Iløpet av prosjektet er det utviklet nye teknologier som gjør det enklere å oversette grid programvare mellom forskjellige grid infrastruktur, dette gjøre at en kan utnytte eksisterende grid infrastruktur mer effektivt. Det har blitt skrevet to Ph.D. avhandlinger under prosjektet. Ph.D. kandidaten Florian Mantz har forsket på hvordan en kan endre systemer slik at de gjenspeiler endringer i krav eller underliggende modelerings formalismer. Han har skrevet en Ph.D avhandling med tittel ?Coupled Transformations of Graph Structures applied to Model Migration?. Ph.D kandidaten Piotr Kazmierczak has studert hvordan sammenkoplede systemer kan modeleres ved hjelp av programvareagenter som tilfredstiller visse sosialelover. Han har skrevet en PhD. avhandling med tittel ?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