Formella metoder är en samling tekniker och notationer baserade på formell logik och formell semantik, tillämpad på modellering och analys av programvara och hårdvarusystem. Deras huvudsakliga syfte är att tillhandahålla otvetydiga specifikationer för systemkrav. Formell verifiering av kraven gör det möjligt att upptäcka fel och buggar, och särskilt konstruktionsfel som inte lätt kan upptäckas bara med test eller simulering. Kursen ger en bred introduktion till ämnet som täcker principerna och algoritmiska metoderna bakom verktygen för mjukvaruanalys och verifiering. I synnerhet beaktas deduktiv verifiering baserad på Hoare-logik och modell-provning baserad på temporallogik.
Kursen ges varje år i period 1, tillsammans med kursen med samma namn på avancerad nivå.
Kursupplägg
Kurslitteratur
Delar av boken Michael Huth, Mark Ryan: Logic in Computer Science, samt diverse papper.
Efter genomgången kurs ska eleverna kunna:
En kurs i logik, motsvarande kursen DD1350 Logik för dataloger.
När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.
Examinator beslutar, baserat på rekommendation från KTH:s handläggare av stöd till studenter med 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.
Man måste klara hemtalen, laborationsuppgifterna och hemtentan.
