Enkeltfag Engelsk 7.5 ECTS

Model tjek

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.

See course description in English

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.

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.

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 sandsynlighedsteori. De studerende skal kunne udtrykke sig i et programmeringssprog.

Forelæsninger, teoretiske øvelser og praktiske øvelser.