02246 Model tjek

2024/2025

Kursusinformation
Model Checking
Engelsk
7,5
Kandidat
Kurset udbydes som enkeltfag
Retningsspecifikt kursus (MSc), Computer Science and Engineering
Retningsspecifikt kursus (MSc), Mathematical Modelling and Computation
Teknologisk specialisering (MSc), Computer Science and Engineering
Teknologisk specialisering (MSc), Mathematical Modelling and Computation
E4B (fre 8-12)
Campus Lyngby
Forelæsninger, teoretiske øvelser og praktiske øvelser.
13-uger
E4B, Afhængigt af antallet af studerende kan der være behov for også at aftale andre dage.
Mundtlig eksamen og bedømmelse af rapport(er)
Alle hjælpemidler - med adgang til internettet
7-trins skala , ekstern censur
02141 , De studerende forventes at kende til endelige automater og/eller transitionssystemer; denne baggrund kan fås i kursus 02141. De studerende forventes at have basal viden om logik og sandsynlighedsteori. De studerende skal kunne udtrykke sig i et programmeringssprog.
Alberto Lluch Lafuente , Lyngby Campus, Bygning 321, Tlf. (+45) 4525 3736 , albl@dtu.dk
Andrey Rivkin , Lyngby Campus, Bygning 321 , ariv@dtu.dk
01 Institut for Matematik og Computer Science
https://courses.compute.dtu.dk/02246
I studieplanlæggeren
Overordnede kursusmål
Modeltjek er modellering og analyse teknikker baseret, bl.a., på logik, graph-baseret modeller (automater, transistionssystemer, Markov chains,...), sandsynlighedsteori, constraint solving, kunstig intelligens 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.). De studerende vil også forstå, hvordan modelkontrol supplerer andre formelle metodeteknikker, og de vil forstå forbindelserne til andre områder såsom kunstig intelligens.
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
02. maj, 2024