Hoppa till huvudinnehåll
Länkstig

Formella metoder i mjukvaruutveckling

Kurs
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-18657
Ansökan stängd

Om utbildningen

  • Kursens syfte är att lära ut kunskap, teknik och omdöme angående viktiga teknikerinom 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örverifikation 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.