Modellbaserad felinjicering och formell verifiering i verktyget SCADE

Bakgrund

Kostnaden för att bygga bort defekter som påträffas under utvecklingsarbetet ökar exponentiellt med den tid projektet fortgår. Detta medför att defekter som kan upptäckas redan i designfasen (modelleringsfasen) sparar både tid och pengar. För att hitta defekter och att verifiera/validera att det utvecklade systemet kan detektera och hantera fel (t.ex. felaktiga specifikationer eller fel i hårdvara) kan man därför injicera fel, alternativt formellt verifiera, en modell av systemet och därefter analysera hur modellen beter sig.

Mål

Målen med examensarbetet är att:
• Studera modelleringsverktyget SCADE och vårt felinjiceringsverktyg FISCADE (som är skrivet i programspråket TCL och som automatiskt injicerar fel i SCADE modeller).
• Utvärdera hur formella metoder kan komplettera felinjiceringsexperiment.
• Vidareutveckla felinjiceringsverktyget genom att:
o analysera vilka fel som kan vara intressanta att köra
o förfina mekanismer för felinjicering
o förbättra det grafiska användargränssnittet som hjälper användaren att konfigurera och automatiskt köra felinjiceringsexperiment
o använde en databas som lagrar resultaten från experimenten
o skriva funktioner som analyserar resultaten

Projektplan

Vi söker två stycken studenter med goda kunskaper inom programmering. Projektarbetet bör motsvara 40 högskolepoäng (20 poäng per student) och kan startas relativt omgående. Slutrapporten skall skrivas fortlöpande under arbetets gång med regelbunden feedback från handledaren på SP. Eftersom detta arbete är av forskningskaraktär är en alltför detaljerad tidsplan inte möjlig att skriva i startskedet.

Arbetet skall utföras i Lindholmen Science Park, Göteborg

Handledare Jonny Vinter, SP Elektronik ([email protected]).

Examinator Håkan Edler, SP Elektronik ([email protected]).