De studerende vil lære at forstå og bruge moderne process orienterede teknikker indenfor modellering, specifikation og validering/verifikation af systemer, såsom service orienterede eller indlejrede systemer. Metoderne vil omfatte rent diskrete teknikker såvel som stokastiske teknikker. En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:

• forklare de vigtigste karakteristika ved de behandlede systemer, herunder reaktive systemer som service orienterede og indlejrede systemer;
• forklare de fundamentale begreber i den proces orienterede tilgang;
• forklare de behandlede proces orienterede sprog og anvende dem til at modellere f.eks. service orienterede og indlejrede 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, såsom service orienterede eller indlejrede systemer.
(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. Uddrag af relevante lærebøger, fx Baier & Katoen: Principles of Model Checking, MIT Press. 28. oktober, 2016