Text

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.

    • Beslutsdatum: 2019-06-24
    • Senaste uppdatering: 2019-06-26

    Referenslitteratur

    Bérard, Béatrice

    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

    Related to Module 1:

    (optional)

    The book can be ordered from Internet via Akademibokhandeln. Please contact them for more information.

    Ernberg, Patrik; Fredlund, Lars-Åke; Hansson, Hans; Jonsson, Bengt; Orava, Fredrik; Perhson, Björn

    Guidelines for Specification and Verification of Communication Protocol

    URL: Länk

    Related to Module 1:

    (optional)

    Clarke, E. M.; Emerson, E. A.; Sistla, A. P.

    Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications

    URL: Länk

    Related to Module 1:

    (optional)

    Jonsson, Bengt

    Course Notes for Reactive Systems

    URL: Länk

    Related to Module 1:

    (optional)

    Larsen, Kim; Pettersson, Paul; Yi, Wang

    UPPAAL in a Nutshell,

    Springer International Journal of Software Tools for Technology Transfer, 1(1-2), 1997

    URL: Länk

    Related to Module 2:

    (otional)

    pages 134-152

    Behrmann, Gerd; David, Alexandre; Larsen, Kim G.

    Tutorial on Uppaal

    In proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT’04). LNCS 3185.,

    URL: Länk

    Related to Module 2

    (optional)

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.

Handbok under studietiden

Betyg

Tvågradig skala

Ö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.