Implementation av membership protokoll i verktyget SCADE

Bakgrund
Sektionen för programvara på SP (Sveriges Provnings- och Forskningsinstitut - http://www.sp.se ) i Borås använder modelleringsverktyget SCADE i två forskningsprojekt. Detta är ett verktyg för bl. a. modellbaserad utveckling, kodgenering samt verifiering. Avancerad programvara i framtidens fordon kommer att utvecklas på detta vis med kodgenerering utifrån modeller.
Distribuerade styrsystem i framtida fordon innehåller applikationer vars olika delar exekverar på flera olika enheter i systemet. En distribuerad programvara måste kunna skicka information mellan olika fysiska enheter och dess arbetsmod kommer att delvis vara beroende av resultat från andra enheter. Här utgör kommunikationen en mycket viktig del av systemet. För att samverkan mellan utspridda delar av en applikation skall ske krävs vissa tjänster i s.k. middleware. Exempel på en sådan är membership.
En membership algoritm finns redan. Projektet går ut på att göra en modell av algoritmen i SCADE för att möjliggöra formell verifiering. I ett senare skede skall kod genereras ur modellen och implementeras i en existerade miljö med distribuerade noder. Målsystemet existerar och används inom forskning och av industri. Det består av noder med MPC565 processorer och ett kommunikationsnätverk med t.ex. Flexray.

Mål
Målen med examensarbetet är att:
- Implementera ett membership-protokoll i SCADE.
- Definiera och ta fram olika testfall, felmodeller och feltillstånd.
- Formellt verifiera protokollet.
- Eventuell modifiering av protokollet.
- Kodgenerering i SCADE.
- Implementation i målsystemet.
- Mätning av resultat.

Projektplan
Projektet är tänkt för två examensarbetare 20p var och kan startas omgående och bör slutföras senast december 2006. Slutrapporten skall skrivas fortlöpande under arbetets gång med regelbunden feedback från handledaren på SP och samordning med närliggande examensarbeten.
Eftersom detta arbete är av forskningskaraktär är en alltför detaljerad tidsplan inte möjlig att skriva i startskedet. Det är en fördel om ni läst kursen ”feltoleranta datorsystem” och/eller kurs i formella metoder el. liknande. Tilltänkt examinator finnes.
Mer information från Carl Bergenhem (tel 033-16 55 53, epost: [email protected])