Kursplan - Avancerad validering och verifiering

Syfte

Verifiering och validering av programvara fokuserar på att upptäcka eventuella buggar i programvaran innan den implementeras, vilket är avgörande för industrin. Syftet med kursen är att ge fördjupade kunskaper inom några av de teorier som ligger bakom mjukvarumodellering och uttömmande verifiering genom formella tekniker. Studenterna kommer att få insikt i forskning och kunna använda verktyg för formell verifiering av diskreta system och realtidssystem.

Lärandemål

Efter avslutad kurs ska studenten kunna:

1. beskriva hur formella modelleringsprå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 de principer som används för att verifiera modeller med model-checking och deduktiv verifiering samt
5. använda verktyg för att modellera och verifiera diskreta system och realtidssystem.

Innehåll

Kursen omfattar följande ämnen: transitionssystem , modal logik, modellering, verifiering med model-checking
och deduktiv formell verifiering. Verktygen UPPAAL och PVS (eller motsvarande) används i kursen.

Undervisning

Föreläsningar och laborationer.

Särskild behörighet

Minst 120 hp varav minst 60 hp inom datavetenskap. Diskret matematik 7,5 hp. 

Dessutom krävs Sv B/Sv 3 samt En A/En 6. I de fall kursen ges på engelska görs undantag från Sv B/Sv 3.  
 

Examination

Laboration (LAB1), 3,5 hp, (examinererar lärandemål 3 och 5), betyg Underkänd (U) eller Godkänd (G)
Tentamen (TEN1), Salstentamen, 4 hp, examinererar lärandemål 1- 4, betyg Underkänd (U), 3, 4 eller 5.

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

Med beröm godkänd, icke utan beröm godkänd, godkänd, underkänd

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

Kursen överlappar helt med DVA402 Avancerad programverifiering och validering.