DD2452 Formella metoder 7,5 hp

Formal Methods

Formella metoder utgör en samling av tekniker och notationer baserade på formell matematisk logik och formell semantik, tillämpad på modellering och analys av mjukvaru- och hårdvarusystem. Deras huvudsyfte är att erbjuda entydiga specifikationer för systemkrav. Formell verifiering av kraven gör det möjligt att upptäcka fel och buggar, särskilt designfel som inte lätt kan upptäckas med hjälp av enbart testning eller simulering. Kursen ger en bred introduktion till ämnet, som täcker principerna och algoritmiska metoderna bakom verktygen för mjukvaruanalys och verifikation. I synnerhet kommer deduktiv verifiering baserad på Hoares-logik och modellkontroll baserad på temporallogik att betraktas.

  • Utbildningsnivå

    Avancerad nivå
  • Huvudområde

  • Betygsskala

    A, B, C, D, E, FX, F

Kurstillfällen/kursomgångar

HT19 form19 för programstuderande

  • Perioder

    HT19 P1 (7,5 hp)

  • Anmälningskod

    50284

  • Kursen startar

    2019-08-26

  • Kursen slutar

    2019-10-25

  • Undervisningsspråk

    Engelska

  • Studielokalisering

    KTH Campus

  • Undervisningstid

    Dagtid

  • Undervisningsform

    Normal

  • Antal platser

    Ingen begränsning

  • Planerade moduler

    P1: I1, D2, F2. mer info

  • Kursansvarig

    Dilian Gurov <dilian@kth.se>

  • Lärare

    Musard Balliu <musard@kth.se>

  • Målgrupp

    Studenter på masterprogram.

  • Del av program

HT18 form18 för programstuderande

Lärandemål

Kursens övergripande syfte är att ge en fungerande förtrogenhet med de huvudsakliga metoderna och verktygen inom det formella metod-området, både teoretiskt och i praktiken.

Efter godkänd kurs ska studenterna kunna:

1. självständigt väja en lämplig modelleringsansats för ett givet enkelt problem,

2. informellt och formellt argumentera för det valda tillvägagångens sundhet och begränsningar,

3. identifiera, specificera och verifiera viktiga systemegenskaper med hjälp av lämpliga automatiserade eller semi-automatiserade verktyg,

4. korrekt tolka och utvärdera analysens resultat.

För att bli godkänd på kursen måste studenten visa förmåga att tillämpa metoderna som diskuteras i kursen. För högsta betyg måste studenten också vara skicklig i det teoretiska fundamentet för dessa metoder.

Kursens huvudsakliga innehåll

Del I. Hoarelogik och deduktiv verifikation

1. Kodannotation: Java-modelleringsspråket JML
2. Automatiserad statisk analys: Svagaste förutsättningar
3. Korrekthet-vid-byggesmetoden till programmering
4. Spöktillstånd och kontrollflödesabstraktion
5. Modelltillstånd och dataabstraktion
6. Back-end: Automated Theorem Proving

Del II. Temporallogik och modellprovning

7. Kripkestrukturer och systemmodellering
8. Temporallogik och modellprovning: LTL och CTL
9. Mjukvarumodellprovning

Kursupplägg

- 7 tvåtimmars föreläsningar
- 7 tvåtimmars övningar
- 6 hemtal, kamraträttade under övningstillfällen
- 2 labbuppgifter
- 1 femtimmars skriftlig tentamen

Behörighet

En kurs i diskret matematik, t.ex. SF1630.

Rekommenderade förkunskaper

Bra kunskaper i logik för dataloger och diskret matematik krävs, t.ex. motsvarande kurserna DD1350 och SF1630.

Litteratur

Föreläsningsanteckningar.

Examination

  • HEMA - Hemuppgifter, 2,5, betygsskala: P, F
  • LABA - Laborationer, 2,5, betygsskala: A, B, C, D, E, FX, F
  • TENA - Tentamen, 2,5, betygsskala: A, B, C, D, E, FX, F

Krav för slutbetyg

Man måste bli godkänd på hemtalen, laborationerna och sluttentan.

Ges av

EECS/Datavetenskap

Kontaktperson

Dilian Gurov, tel: 790 8198, e-post: dilian@kth.se

Examinator

Dilian Gurov <dilian@kth.se>

Versionsinformation

Kursplan gäller från och med VT2019.
Examinationsinformation gäller från och med VT2019.