Overordnede kursusmål
Modeltjek er modellering og analyse teknikker baseret, bl.a., på
logik, graph-baseret modeller (automater, transistionssystemer,
Markov chains,...), sandsynlighedsteori og spil teori. De
studerende vil lære at bruge modeltjek teknikker til modellering,
specifikation og validering/verifikation for forskellige klasser af
systemer (distribuerede/parallele systemer, schedulers,
controllers, netværk, biologiske systemer, spil, osv.)
Læringsmål
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
- forklare de vigtigste karakteristika ved de behandlede
systemer;
- forklare de fundamentale begreber i den proces orienterede
tilgang til modellering, specifikation og validering/verifikation
af systemer;
- forklare de behandlede proces orienterede sprog og anvende dem
til at modellere systemer;
- forklare de behandlede logikker og bruge dem til at specificere
egenskaber relateret til f.eks. robusthed, sikkerhed og
ydelse;
- anvende moderne værktøjer til validering af modeller og
forklare den overordnede virkemåde for sådanne værktøjer;
- identificere situationer hvor kursets teknikker er
anvendelige;
- motivere og designe en valideringsproces, f.eks. en serie af
værktøjsbasserede eksperimenter, og fortolke de opnåede
resultater;
- opnå disse resultater gennem en gruppe indsats, under
opretholdelse af individuelt ansvar;
- kommunikere de opnåede resultater klart og præcist gennem en
teknisk rapport i standard format.
Kursusindhold
Kurset dækker tre hovedemner:
(1) Metoder til modellering af systemer med aspekter som
non-determinism, probabilistiske / stokastiske aspekter og
forskellige agenter/mål (spil): transition systemer, Markov
modeller, og games.
(2) Logiske formalismer til at udtrykke egenskaber relateret til
korrekthed, sikkerhed og ydelse af systemer.
(3) Validerings og verifikations værktøjer der kan afdække
forholdet mellem modeller og egenskaber og dermed give stærke
garantier relateret til korrekthed, sikkerhed eller ydelse.
Litteraturhenvisninger
Uddrag af relevante lærebøger, fx Baier & Katoen: Principles of
Model Checking, MIT Press.
Sidst opdateret
27. april, 2022
