Hoppa till huvudinnehållet

DD2452 Formella metoder 7,5 hp

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.

Kursomgångar saknas för tidigare och kommande terminer, samt för innevarande termin.
Rubriker med innehåll från kursplan DD2452 (VT 2019–) är markerade med en asterisk ( )

Innehåll och lärandemål

Kursinnehå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

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.

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

Kurslitteratur och förberedelser

Särskild 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.

Utrustning

Ingen information tillagd

Kurslitteratur

Föreläsningsanteckningar.

Examination och slutförande

När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.

Betygsskala

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

Examination

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

Examinator beslutar, baserat på rekommendation från KTH:s samordnare för funktionsnedsättning, om eventuell anpassad examination för studenter med dokumenterad, varaktig funktionsnedsättning.

Examinator får medge annan examinationsform vid omexamination av enstaka studenter.

Övriga krav för slutbetyg

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

Möjlighet till komplettering

Ingen information tillagd

Möjlighet till plussning

Ingen information tillagd

Examinator

Profile picture Dilian Gurov

Etiskt förhållningssätt

  • Vid grupparbete har alla i gruppen ansvar för gruppens arbete.
  • Vid examination ska varje student ärligt redovisa hjälp som erhållits och källor som använts.
  • Vid muntlig examination ska varje student kunna redogöra för hela uppgiften och hela lösningen.

Ytterligare information

Kurswebb

Ytterligare information om kursen kan hittas på kurswebben via länken nedan. Information på kurswebben kommer framöver flyttas till denna sida.

Kurswebb DD2452

Ges av

EECS/Datavetenskap

Huvudområde

Datalogi och datateknik

Utbildningsnivå

Avancerad nivå

Påbyggnad

Ingen information tillagd

Kontaktperson

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

Övrig information

I denna kurs tillämpas EECS hederskodex, se:
http://www.kth.se/eecs/utbildning/hederskodex