Kursplan fastställd 2019-02-21 av programansvarig (eller motsvarande).
Kursöversikt
- Engelskt namnFormal Methods in Software Development
- KurskodTDA294
- Omfattning7,5 Högskolepoäng
- ÄgareMPALG
- UtbildningsnivåAvancerad nivå
- HuvudområdeDatateknik, Informationsteknik
- InstitutionDATA- OCH INFORMATIONSTEKNIK
- BetygsskalaTH - Mycket väl godkänd (5), Väl godkänd (4), Godkänd (3), Underkänd
Kurstillfälle 1
- Undervisningsspråk Engelska
- Anmälningskod 02129
- Blockschema
- Sökbar för utbytesstudenterNej
Poängfördelning
Modul | LP1 | LP2 | LP3 | LP4 | Sommar | Ej LP | Tentamensdatum |
|---|---|---|---|---|---|---|---|
| 0117 Muntlig tentamen 5 hp Betygsskala: TH | 5 hp | ||||||
| 0217 Laboration 2,5 hp Betygsskala: UG | 2,5 hp |
I program
- MPALG - DATAVETENSKAP - ALGORITMER, PROGRAMSPRÅK OCH LOGIK, MASTERPROGRAM, Årskurs 1 (obligatoriskt valbar)
- MPALG - DATAVETENSKAP - ALGORITMER, PROGRAMSPRÅK OCH LOGIK, MASTERPROGRAM, Årskurs 2 (valbar)
- MPSOF - SOFTWARE ENGINEERING AND TECHNOLOGY - UTVECKLING OCH IMPLEMENTERING AV MJUKVARA, MASTERPROGRAM, Årskurs 2 (valbar)
Examinator
Wolfgang Ahrendt- Viceprefekt, Data- och informationsteknik
Behörighet
Grundläggande behörighet för avancerad nivåSökande med en programregistrering på ett program där kursen ingår i programplanen undantas från ovan krav.
Särskild behörighet
Engelska 6Sökande med en programregistrering på ett program där kursen ingår i programplanen undantas från ovan krav.
Kursspecifika förkunskaper
Kursen kräver förkunskaper inom logik, DAT060 Matematisk logik för datavetenskap eller SSY165 Händelsediskreta system. Kännedom om objektorienterad programmering (t.ex. Java) är också en fördel.Syfte
Kursens syfte ä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.Lärandemål (efter fullgjord kurs ska studenten kunna)
Efter godkänd kurs ska studenten kunna:Kunskap och förståelse
- redogöra möjligheter och begränsningar hos logikbaserade verifikationstekniker föratt bedöma och förbättra mjukvarukvalitet
- avgöra vad som kan och inte kan uttryckas i en given formalism för specifikationeller modellering
- avgöra vad som kan och inte kan analyseras med en given logik och bevismetod
- formellt uttrycka säkerhetsegenskaper och liveness hos (parallella) program
- beskriva grunderna i verifikation av säkerhetsegenskaper och liveness med hjälp av modellkontroll (model checking)
- använda verktyg som automatiserar modellkontroll av säkerhetsegenskaper
- skriva formella specifikationer för klasser i objekt-orienterade program med hjälp av kontrakt och klassinvarianter
- beskriva hur förhållandet mellan program och formell specifikation kan representeras i en programlogik
- verifiera funktionella egenskaper hos enkla Javaprogram med ett verifikationsverktyg.
- bedöma och kommunicera betydelsen och vikten av korrekthet i mjukvaruutveckling
- lösa problem relaterade till utveckling av välfungerande mjukvara genom abstraktion, modellering och rigorösa resonemang.
Innehåll
Kursen behandlar två formella metoder för mjukvara, modellkontroll (model checking) och deduktiv verifikation.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