02141 Datalogisk modellering

2024/2025

Kursusinformation
Computer Science Modelling
Engelsk
10
Bachelor
Teknologiske linjefag, General Engineering
Teknologiske linjefag, Softwareteknologi
Tilvalgskursus (B Eng), Softwareteknologi
Retningsspecifikt kursus (BSc), Softwareteknologi
Retningsspecifikt kursus (BSc), General Engineering
Tilvalgskurser, IT og Økonomi
F3A (tirs 8-12) og F4B (fre 8-12)
Campus Lyngby
Forelæsninger, teoretiske øvelser, programmeringsøvelser og -opgaver.
13-uger
F4B
Skriftlig eksamen og bedømmelse af opgave(r)
Skriftlig eksamen (som normalt ændres til mundtlig ved reeksaminer). Et antal individualiserede programmeringsopgaver vil indgå i den samlede vurdering.
Skriftlig eksamen: 4 timer
Alle hjælpemidler - med adgang til internettet
7-trins skala , ekstern censur
02143
(01001/01019).­02105.­(02100/02157) , Grundlæggende viden om diskret matematik (logik, mængder, grafer, funktioner, induktion) - som forudsat f.eks. i 01001 og 01019 Grundlæggende viden om algoritmer og datastrukturer - som forudsat f.eks. i 02105. Grundlæggende viden om funktionel programmering - som forudsat f.eks. i 02100 og 02157.
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/02141
I studieplanlæggeren
Overordnede kursusmål
De studerende lærer at anvende centrale datalogiske modeller og formalismer, at udvikle værktøjer baseret på disse formalismer og at bruge disse værktøjer til at køre og analysere softwarekode.
Læringsmål
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
  • anføre forskelle i udtrykskraft af de præsenterede formelle modeller;
  • relatere udtryksevne til begrænsninger af beregningsmodeller (f.eks. afgørelighed/​uafgørlighed af grundlæggende problemer)
  • tolke betydningen af en formel model (f.eks. automater, grammatikker, semantikker, transitionsystemer, formelle specifikationer):
  • udlede en formel model (f.eks. automater, grammatiker, semantikker) for en ønsket egenskab eller opførsel givet en tekstuel beskrivelse;
  • oversætte en model til en anden model (f.eks. regulære udtryk til NFA);
  • ændre en model svarende til et givet kriterie (f.eks. fjernelse af redundans, fjernelse af flertydighed i grammatik);
  • anvende udvalgte værktøjer og udvikle nye værktøjer baseret på de formelle modeller for at køre og analysere programmer (f.eks. compilere, tolke, programverifikatorer, analysatorer og modeltjekkere)
  • afgøre om en beskrivelse i en formel model opfylder en givet egenskab;
  • udlede egenskaber af formelle modeller ved at anvende bevisstrategier (f.eks. matematisk induktion, strukturel induktion);
  • udlede egenskaber af programmer ved hjælp af automatiserede formelle metoder;
  • vælge formelle modeller der kan være nødvendige eller nyttige ved løsning af et givent problem;
Kursusindhold
Kurset omfatter to emner:

(1) Formelle sprog og deres brug til at beskrive syntaks. For regulære sprog behandles måder at beskrive dem med automata og regulære udtryk, deres sammehæng, praktiske anvendelser (fx søgning, leksikalsk analyse, formelle specifikationer) og nogle væsentlige teoretiske resultater (fx herunder afgørlighedsegenskaber af væsentlige problemer). For kontekstfri sprog behandles måder at beskrive dem med pushdown automata og kontekstfri grammatik, en række anvendelser (fx til parsing af programmer, dokumenter og formateret data) sammen med en kort indføring til stakautomater og deres sammenhæng med kontekstfri sprog.

(2) Formelle metoder og deres brug til både modellering og analyse af IT systemers egenskaber, især software kode. Dette omfatter semantik af programmeringssprog og dets brug til at bygge compilere og tolke, såvel som deres brug som grundlag for automatiserede metoder til at analysere programmer. Vi vil især dække programverifikation, programanalyse, sikkerhedsanalyse og modeltjek.

Kurset involverer praktisk brug af forskellige værktøjer, og de studerende skal løse både teoretiske og praktiske opgaver, som integrerer kursets to emner. Til sidst dækker vi nogle grundlæggende praktiske og teoretiske aspekter af formelle sprog (f.eks. pumping lemma, Turing-maskiner, minimering af automater).
Litteraturhenvisninger
(1) "Introduction to Automata Theory, Languages, and Computation", af John E. Hopcroft, Rajeev Motwani, Jefrey D. Ullman, Third Edition, Addison-Wesley, 2007.
Kursusbogen "02141: Automata Theory and Languages" udvalgt af Hanne Riis Nielson indeholder de nødvendige kapitler.
(2) "Formal Methods - An Appetizer" af Flemming Nielson og Hanne Riis Nielson, Springer, 2019. Videoer på YouTube kanalen FormalMethodsDK. Slides og on-line systemer på FormalMethods.dk
Bemærkninger
Kurset gives på engelsk.
Sidst opdateret
06. januar, 2025