Formella metoder i mjukvaruutveckling
Om utbildningen
Syftet med denna kurs är att lära ut kunskap, teknik och omdöme angående viktiga tekniker inom formella metoder: modellkontroll (model checking) och deduktiv verifikation.
Båda stilarna introduceras på tre sätt: konceptuellt, teoretisk och praktiskt, genom användning av ett specifikt verktyg. Kursen bygger på kunskap om första ordningens logik och temporallogik, och visar hur dessa formalismer kan appliceras, och utökas för verifikation av mjukvara.
För modellkontroll täcker kursen följande ämnen:
- ett specifikationsspråk för parallella processer,
- verifiering av påståenden,
- synkronisering,
- verifikation av säkerhets- och livenessegenskaper som är skrivna i temporal logik.
För deduktiv verifikation täcker kursen följande ämnen:
- ett specifikationsspråk på enhetsnivå för Java-program,
- en logik för verifikation av Java-program,
- verifikation av Java-program, i meningen att implementationen av en enhet uppfyller dess specifikationen.
Behörigheter och urval
Förkunskapskrav
Godkända kurser om 120 hp i ämnet Datavetenskap, eller motsvarande, särskilt DIT201 Logic in Computer Science, 7,5 hp, och en 7,5 hp kurs i objektorienterad programmering (eller motsvarande) är ett krav. Dessutom krävs språkkunskaper motsvarande Engelska 6/Engelska B.
Urval
Högskolepoäng, max 165 hp.
