Kursplan - Formell verifiering av reaktiva system

Syfte

Verifiering och validering av programvara fokuserar på att upptäcka eventuella fel i programvaran innan den implementeras, vilket är avgörande för industrin. Syftet med kursen är att introducera studenterna till metoder och verktyg för att verifiera system som skall reagera på yttre stimuli. Metoderna använder systemmodeller med precis formell semantik och sträcker sig över kontraktbaserad verifiering, model checking samt deduktiv verifiering. Studenterna kommer att lära sig teorier om formell verifiering, och hur man använder verktygsstöd för att verifiera systemmodeller samt program.

Lärandemål

Efter avslutad kurs skall studenten kunna:

1. beskriva hur formella modelleringsspråk kan användas för att modellera system
2. modellera diskreta system och realtidssystem med hjälp av finita tillståndsmaskiner och tidsautomater
3. specificera enkla systemkrav med temporal logik
4. beskriva principerna för att verifiera modeller med model checking och deduktiv verifiering
5. beskriva principerna för kontraktbaserad verifiering av program
6. använda verktyg för att modellera och verifiera diskreta system och realtidssystem
7. använda kontrakt-baserade verktyg för att verifiera program (t.ex., i C)
 
 
 
 

Innehåll

Kursen omfattar följande ämnen: transitionssystem, modal logik, modellering, verifiering med model-checking, deduktiv formell verifiering och kontrakt-baserad verifiering av program.  
Exempel på verktyg som kommer att användas i kursen är: UPPAAL, PVS, VCC, Dafny etc.
 

Undervisning

Föreläsningar (webbaserade).

Särskild behörighet

120 hp, varav 80 hp inom teknik eller informatik, inklusive minst 30 hp programmering eller mjukvaruutveckling.
Dessutom minst 18 månaders dokumenterad erfarenhet av arbete med mjukvaruutveckling eller relaterad verksamhet. Dessutom krävs Svenska B/Svenska 3 samt Engelska A/Engelska 6. I de fall kursen ges på engelska görs undantag från kravet på Svenska B/Svenska 3.
 

Examination

Inlämningsuppgift (INL1), Skriftlig inlämningsuppgift, 2,5 hp, (examinerar lärandemål 1 och 2), Betyg Underkänd (U) eller Godkänd (G)
Inlämningsuppgift (INL2), Skriftlig inlämningsuppgift, 2,5 hp, (examinerar lärandemål 3, 4 och 6), Betyg Underkänd (U) eller Godkänd (G)
Inlämningsuppgift (INL3), Skriftlig inlämningsuppgift, 2,5 hp, (examinerar lärandemål 5 och 7), Betyg Underkänd (U) eller Godkänd (G)

En student som har ett intyg från MDU avseende sin funktionsnedsättning har möjlighet att anmäla önskemål om anpassning vid salstentamina eller annan examinationsform i enlighet med Regler och anvisningar för examination på grundnivå och avancerad nivå vid Mälardalens högskola (2020/1655). Det är examinator som, utifrån det intyg som utfärdats, beslutar om eventuell anpassning och i så fall vilken anpassning som ska gälla.

Misstankar om vilseledande vid examination (fusk) anmäls, enligt högskoleförordningen, till universitetets rektor och prövas av universitetets disciplinnämnd. Om disciplinnämnden anser att en student gjort sig skyldig till en disciplinförseelse fattar nämnden beslut om en disciplinär åtgärd, vilket är varning eller avstängning.

Betyg

Godkänd, underkänd

Övergångsbestämmelser och övriga föreskrifter

Kursen överlappar med 2,5 hp mot kursen Avancerad validering och verifiering 7,5 hp.