Kursplan för Formella metoder i mjukvaruutveckling

Kursplan fastställd 2021-02-26 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 02134
  • Blockschema
  • Sökbar för utbytesstudenterJa

Poängfördelning

0117 Muntlig tentamen 5 hp
Betygsskala: TH		5 hp
0217 Laboration 2,5 hp
Betygsskala: UG		2,5 hp

I program

Examinator

Gå till kurshemsidan (Öppnas i ny flik)

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 6
Sö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
Färdigheter och förmåga
  • 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.
Värderingsförmåga och förhållningssätt
  • 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

Organisation

Det är cirka två föreläsningar per vecka och det finns en övning per vecka. Studenterna utför praktiska exempelövningar med hjälp av verktygen i laborationer.

Litteratur

Se separat literaturlista.

Examination inklusive obligatoriska moment

Kursen bedöms genom två inlämningsuppgifter som normalt genomföras i grupper om två, samt en muntlig tentamen vid kursens slut. Inlämningsuppgiter och muntlig tentamen kan godkännas oberoende av varandra. För att få godkänt på hela kursen krävs godkänt på både inlämningsuppgifterna och den muntlig tentamen. Betyg för godkända studenter avgörs av tentamensresultatet.

Kursens examinator får examinera enstaka studenter på annat sätt än vad som anges ovan om särskilda skäl föreligger, till exempel om en student har ett beslut från Chalmers om pedagogiskt stöd på grund av funktionsnedsättning.