Formella metoder i mjukvaruutveckling

Kursen kan ingå i följande program:

1. Computer Science, Master's Programme (N2COS)
2. Datavetenskapligt program (N1COS)

Kursen ges även som fristående kurs vid Göteborgs Universitet.

Godkända kurser om 120 hp i ämnet Datavetenskap, eller motsvarande, särskilt DIT201 Logic in Computer Science, 7,5 hp, och en 7,5 hp kurs i objektorienterad programmering (eller motsvarande) är ett krav.

Följande kunskapsnivå i Engelska krävs: Engelska 6/Engelska nivå 2 eller motsvarande från ett erkänt internationellt test, t.ex. TOEFL, IELTS.

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.

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:

• programlogik, inklusive Hoare-logik och separationslogik,
• resonemang om loopar med invarianter,
• verifikation av små program med programverifikationsverktyg,
• tekniker som används vid verifikation av större eller komplexare program

Efter godkänd kurs ska studenten kunna:

Kunskap och förståelse

• redogöra möjligheter och begränsningar hos logikbaserade verifikationstekniker för att bedöma och förbättra mjukvarukvalitet,
• avgöra vad som kan och inte kan uttryckas i en given formalism för specifikation eller 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 program i 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.

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.

Undervisningsspråk: engelska

Kursen examineras genom en skriftlig salstentamen vid slutet av kursen och obligatoriska inlämningsuppgifter som lämnas in under kursens gång. Inlämningsuppgifterna görs vanligtvis i par.

Om en student som har underkänts två gånger på samma examinerande moment önskar byta examinator inför nästa examinationstillfälle ska en sådan begäran bifallas om det inte finns särskilda skäl däremot (6 kap. 22 § HF).

Om en student har fått besked om pedagogiskt stöd från Göteborgs universitet med rekommendation om anpassad examination och/eller anpassad examinationsform kan examinator, i det fall det är förenligt med kursens lärandemål och förutsatt att inte orimliga resurser krävs, besluta att bevilja studenten anpassad examination och/eller anpassad examinationsform.

Om en kurs har avvecklats eller genomgått en större förändring ska studenten erbjudas minst två examinationstillfällen, utöver ordinarie examinationstillfälle. Dessa tillfällen fördelas under en tid av minst ett år, dock som längst två år efter det att kursen avvecklats/förändrats. Vad gäller praktik och verksamhetsförlagd utbildning (VFU) gäller motsvarande, men med begränsning till endast ett ytterligare examinationstillfälle.

Om en student har fått besked om att denne uppfyller kraven för att vara student vid Riksidrottsuniversitetet (RIU-student) har examinator rätt att besluta om anpassning vid examination, om detta görs i enlighet med Lokala regler gällande RIU-studenter vid Göteborgs universitet

Delkurser

1. Skriftlig salstentamen, 5 hp
   Betygsskala: Mycket väl godkänd (5), Väl godkänd (4), Godkänd (3) och Underkänd (U)
2. Laboration, 2,5 hp
   Betygsskala: Godkänd (G) och Underkänd (U)

På kursen ges något av betygen Mycket väl godkänd (5), Väl godkänd (4), Godkänd (3) och Underkänd (U).

För att få godkänt på hela kursen krävs godkänt på både inlämningsuppgifterna och den skriftliga salstentamen. Betyg för godkända studenter avgörs av tentamensresultatet.

Kursen utvärderas genom möten, både under och efter kursen, mellan lärare och studentrepresentanter. Ett anonymt skriftligt frågeformulär skickas även ut till studenterna efter kursens slut. Resultaten av utvärderingarna används för att förbättra kursinnehållet och som indikation till vilka delar som skulle kunna läggas till, tas bort, förbättras eller ändras.

Kursen är en samläst kurs med Chalmers.

Kursen ersätter DIT271 Software Engineering using Formal Methods. Den här kursen kan inte ingå i en examen som innehåler DIT271. Den kan inte heller ingå i en masterexamen som bygger på en annan bachelorexamen där DIT271 ingår.