DD2452 Formella Metoder

Kursanalys VT08

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

Inga.

Sammanfattning

Jag anser att kursen gick gick hyfsat bra, men man borde kanske ta bort den andra kursdelen och gå djupare i del ett och tre.

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.

Ny betygsskala A-F

Jag har inte lyckats än att formulera en tabell som definerar vad exakt man bor kunna för att få ett visst betyg. Jag anser att detta inte är så lätt för den här kursen, därför använde jag mig av en finare, fast fortfarande lineär skala baserad på poäng. Nästa omgång ska jag försöka införa en betygstabell.

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

Elevenkätet visar att studenterna uppskattade kursen. Dokumentationen till de olika verktygen behöver kanske förbättras. 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

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

Övrigt

Inga komentarer för tillfället.

Planerade förändringar

På grund av dålig budget kommer kursens omfattining att minskas betydligt. Jag funderar på att minska breden på materialet genom att ta bort del två, och gå djupare i del ett och tre. Jag letar också efetr en ny kursbok.