Cristin-prosjekt-ID: 442678
Sist endret: 13. desember 2018 13:32

Cristin-prosjekt-ID: 442678
Sist endret: 13. desember 2018 13:32
Prosjekt

Formal Modelling and Verification of Grid Systems

prosjektleder

Yngve Lamo
ved Institutt for datateknologi, elektroteknologi og realfag ved Høgskulen på Vestlandet

prosjekteier / koordinerende forskningsansvarlig enhet

  • Høgskulen på Vestlandet

Finansiering

  • TotalbudsjettNOK 4.700.000
  • Norges forskningsråd
    Prosjektkode: 194521

Kategorier

Prosjektkategori

  • Bidragsprosjekt

Tidsramme

Avsluttet
Start: 14. april 2009 Slutt: 13. april 2014

Beskrivelse Beskrivelse

Tittel

Formal Modelling and Verification of Grid Systems

Vitenskapelig sammendrag

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?

Tittel

Formal Modelling and Verification of Grid Systems

Vitenskapelig sammendrag

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

prosjektdeltakere

prosjektleder

Yngve Lamo

  • Tilknyttet:
    Prosjektleder
    ved Institutt for datateknologi, elektroteknologi og realfag ved Høgskulen på Vestlandet
  • Tilknyttet:
    Prosjektdeltaker
    ved Høgskulen på Vestlandet
1 - 1 av 1

Resultater Resultater

Hybrid On-the-Fly Model Checking with the Sweep-line Method.

Kristensen, Lars Michael; Evangelista, Sami. 2012, Lecture Notes in Computer Science (LNCS). HVLVitenskapelig artikkel

A Graphical Approach to Component-based and Extensible Model Checking Platforms.

Kristensen, Lars Michael; Westergaard, Michael. 2011, Lecture Notes in Computer Science (LNCS). TUE, HVLVitenskapelig artikkel

Formal Modelling and Initial Validation of the Chelonia Distributed Storage System.

Kristensen, Lars Michael; Taktak, Sami. 2011, Lecture Notes in Computer Science (LNCS). HVLVitenskapelig artikkel

Automatic Structure-Based Code Generation from Coloured Petri Nets: A Proof of Concept.

Kristensen, Lars Michael; Westergaard, M. 2010, Lecture Notes in Computer Science (LNCS). TUE, HVLVitenskapelig artikkel

A Perspective on Explicit State Space Exploration of Coloured Petri Nets: Past, Present, and Future.

Kristensen, Lars Michael. 2010, Lecture Notes in Computer Science (LNCS). HVLVitenskapelig artikkel
1 - 5 av 5