2D1452 Formella Metoder

Kursanalys VT07

Kursdata

Mål

Kursen är avsedd att ge grundläggande färdigheter i formella metoder för specifikation och verifikation av datorsystem, teori såväl som praktik. Den studerande ska kunna modellera ett enkelt problem med hjälp av lämpliga verktyg, argumentera formellt och informellt för modellens sundhet och begränsningar, samt genomföra en analys av problemet med användning av lämpliga hel- eller halvautomatiska verktyg.

Förändringar inför denna kursomgång

Jag tog över kursen från Mads Dam. Förändringarna som jag genomförde är: jag introducerade en ny kursbok, ändrade ordningen på de tre kursdelarna, och akcenterade mera på modal och temporal logik på bekostnad av automater. Labbdelen är nästan oförändrad.

Sammanfattning

Enligt min uppfattning gick kursen hyfsat bra. Studenternas aktiva deltagande under lektionerna var en klar indikation på detta. Laborationerna gjordes noggrant och i tid.

Undervisningen

Jag brukar blanda föreläsningar med övningar och studenterna verkar uppskatta detta. Jag stimulerar aktivt deltagande för att få direkt feedback och på så sätt hålla koll på hur studenterna följer materialet. Laborationstimmarna är bara till redovisning.

Examination

Examinationen består av en skriftlig tenta som examinerar studenternas teoretiska kunskap och färdigheter inom kursområdet. Själva tentan (med lösningar) finns här.

Laborationer

Kursen inehåller också en labbdel, bestående av tre laborationer. I varje av dem används ett nytt verktyg för att analysera olika aspekter av programbeteende.

Kurslitteratur

I kursen används boken Logic in Computer Science av Michael Huth och Mark Ryan, Cambridge University Press, 2000. Tyvärr finns det ingen bok som passar direkt till hela  kursprogrammet. Det var kanske därför att ungäfer hälften av studenterna aldrig skaffade sig boken. Boken komplementeras med annan material som papper och handouts.

Elevenkät

Studenterna gav höga betyg på nästan alla frågor, men gav också flera konkreta förbättringsföreslag. Hela kursutvärderingen finns här.

Kursens belastning för eleverna

En jämn belastning under kursen. Studenterna har tre laborationer - en efter varje kursdel - som redovisas i datorsalerna.

Förkunskaper

Förkunskaper som är väsentliga för kursen är Diskret Matematik och Logik.

Verkligt kursinnehåll

Verkliga kursinnehållet kan ses på följande länk.

Övrigt

Inga komentarer för tillfället.

Planerade förändringar

Inga större förändringar planeras.