Skriv ut kursplan
Kursplan - Kvalitetssäkring - Upptäcka fel genom formell verifiering
Omfattning
7.5 hp
Kurskod
DVA468
Giltig från
Hösttermin 2018
Utbildningsnivå
Avancerad nivå
Successiv fördjupning
A1N (Avancerad nivå, har endast kurs/er på grundnivå som förkunskapskrav).
Huvudområde(n)
Datavetenskap
Akademi
Akademin för innovation, design och teknik
Fastställd
2018-02-01
Litteraturlistor
Kurslitteraturen är preliminär till 8 veckor innan kursstart. Kurslitteratur kan vara giltig över flera terminer.
-
Referenslitteratur
Systems and software verification : model-checking techniques and tools
Berlin : Springer, cop. 2001 - xii, 190 s.
ISBN: 3-540-41523-8 (alk. paper) ; LIBRIS-ID: 5368361
Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications
URL: Länk
UPPAAL in a Nutshell,
Springer International Journal of Software Tools for Technology Transfer, 1(1-2), 1997
URL: Länk
Tutorial on Uppaal
In proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT04). LNCS 3185.,
URL: Länk
Syfte
Verifiering 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 system- och programverifiering. 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 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 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 kontraktbaserade 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 krävs Svenska B/Svenska 3 samt Engelska A/Engelska 6. I de fall kursen ges på engelska görs undantag från 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 helt mot Formell verifiering av reaktiva system 7,5 hp och Avancerad validering och verifiering 7,5 hp.