Hoppa till huvudinnehåll
Länkstig

Formella metoder i mjukvaruutveckling

Kurs
DIT272
Avancerad nivå
7,5 högskolepoäng (hp)
Studietakt
50%
Undervisningstid
Dag
Studieort
Göteborg
Undervisningsform
Campus
Undervisningsspråk
Engelska
Start/slut
-
Ansökan öppen
-
Anmälningskod
GU-18682
Ansökan öppnar 15 mars 2021

Om utbildningen

Syftet med denna kurs ä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:

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

Behörigheter och urval

Förkunskapskrav

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. Dessutom krävs språkkunskaper motsvarande Engelska 6/Engelska B.  

Urval

Högskolepoäng, max 225 hp

För antagning till sommaren 2021 och framåt gäller följande urval: högskolepoäng, max 165 hp.