Modellbaserad utveckling av membership-protokoll i verktyget SCADE

Bakgrund
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 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 tjänst sådan är membership.
SP (Sveriges Provnings- och Forskningsinstitut) 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.
Arbete kring membership-algoritmer pågår idag. Exjobbet 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ål
Ert arbete skall bestå i något av:
• Implementera ett membership-protokoll i SCADE.
• Definiera och ta fram olika testfall, felmodeller och feltillstånd.
• Formellt verifiera protokollet.
• Kodgenerering i SCADE.
• Implementation i ett målsystem.

Projektplan
Projektet är tänkt för två teknologer (20p var) vid data eller elektroinriktat magister eller civilingenjörsprogram. Slutrapporten skall skrivas fortlöpande under arbetets gång med regelbunden feedback från handledaren på SP och samordning med närliggande examensarbeten.
Det är en fördel om du läst kursen ”feltoleranta datorsystem” och/eller kurs i formella metoder. Placering kommer att vara i Lindholmen Science Park och kan påbörjas omgående. Samordning med flera närliggande examensarbeten kommer att ske.
Mer information från Carl Bergenhem (tel 033-16 55 53, epost: [email protected])