DM861: Concurrency Theory

Indgangskrav

Ingen

Faglige forudsætninger

Studerende, der følger kurset, forventes at: Have et indgående kendskab til diskret matematik.

Formål

Multi-core processorer, cloud computing, og web services gør, at ”concurrent” systemer er udbredte. At designe og programmere disse systemer korrekt er udfordrende. Det kræver, at man kan forudsige, hvordan flere programmer, som udføres selvstændigt, vil interagere med andre programmer.

Dette kursus har til formål at præsentere og undersøge modeller, ræsonnementteknikker og abstrakte programmeringsdiscipliner for

concurrent systemer. Disse værktøjer giver mulighed for at omsætte konkrete krav og design i præcise matematiske definitioner, som kan bruges til at bevise, at de ønskede egenskaber leveres (f.eks deadlockfreedom eller sikker brug af asynkrone kanaler).

Mange af de modeller, som er omfattet i kurset, er grundlaget for nye programmeringssprog og designværktøjer, såsom BPMN, Go og Jolie.

I forhold til uddannelsens kompetenceprofil har kurset eksplicit fokus

på at:

Give kompetence til at: planlægge og udføre videnskabelige projekter på højt fagligt niveau, herunder styre arbejds- og udviklingssituationer, der er komplekse, uforudsigelige og forudsætter nye løsningsmodeller.
Give færdigheder i at: beskrive, analysere og løse avancerede datalogiske problemstillinger ved hjælp af de lærte modeller, udvikle nye varianter af de lærte metoder, hvor et konkret problem kræver det.
Give viden om: et udvalg af specialiserede modeller og metoder udviklet inden for datalogi, baseret på højeste internationale forskning, herunder emner fra fagets forskningsfront; at kunne forstå og på et videnskabeligt grundlag reflektere over det datalogiske fagområdes viden, samt kunne identificere videnskabelige problemstillinger.

Kurset bygger på kompetencer i diskrete matematik fra bacheloruddannelsen. Kursets indhold kan bruges til en speciale i concurrency-området.

Målbeskrivelse

For at opnå kursets formål er det læringsmålet for kurset, at den

studerende demonstrerer evnen til at:

repræsentere reele concurrent systemer i de abstrakte modeller dækket i kurset;
identificere og formalisere typiske nyttige egenskaber af concurrent systemer, ligesom deadlock-freedom;
bevis egenskaber af concurrent systemer;
bevis generelle egenskaber af formelle modeller for concurrency.

Indhold

Kurset indeholder følgende faglige hovedområder:

Procesmodeller for concurrency.
High-level programmeringssprog til concurrent systemer.
Inference-systemer til sikkerhed i concurrency.
Koreografier: sprog, oversættelse og syntese.

Litteratur

Montesi, F. (2023). Introduction to Choreographies. Cambridge University Press. doi:10.1017/9781108981491

Se Itslearning for pensumlister og yderligere litteraturhenvisninger

Eksamensbestemmelser

Eksamenselement a)

Tidsmæssig placering

Juni

Udprøvninger

Skriftlig Eksamen

EKA

N340005102

Censur

Intern prøve, to eller flere bedømmere

Bedømmelse

7-trinsskala

Identifikation

Studiekort - Eksamensnummer

Sprog

Følger, som udgangspunkt, undervisningssprog

Varighed

3 timer

Hjælpemidler

Eksamen er med begrænsede hjælpemidler. Det er kun følgende hjælpemidler som er tilladt:

Ordbøger til oversættelse af sprog (fx dansk/engelsk, dansk/tysk osv.) i ordbogsprogrammet fra http://www.ordbogen.com/ i elektronisk form. Browserudgaven er ikke tilladt. Se komplet liste over, hvilke ordbøger som er tilladt, i den separate "Vejledning til ordbogen dot com". Alle andre ordbøger end de tilladte skal være slået fra i ordbogsprogrammet

Internet er ikke tilladt. Du må dog gå ind på kursets hjemmeside i itslearning i forbindelse med åbning af system "DE – Digital Eksamen" og udfyldelse af evt. test i systemet.

ECTS-point

Uddybende information

Eksamensopgaven er frit format. Eksamensopgaven udleveres som PDF-dokument, og besvarelsen skal afleveres som et samlet PDF-dokument.

Forudsætningsprøve a)

Tidsmæssig placering

Forår

Udprøvninger

Opgaver i løbet af kurset

EKA

N340005112

Censur

Intern prøve, en bedømmer

Bedømmelse

Bestået/Ikke bestået

Identifikation

Fulde navn og SDU brugernavn

Sprog

Følger, som udgangspunkt, undervisningssprog

Hjælpemidler

Oplyses på kurset

ECTS-point

Uddybende information

Forudsætningsprøven er en forudsætning for deltagelse i eksamenselement a)

Vejledende antal undervisningstimer

60 timer per semester

Undervisningsform

På naturvidenskab er undervisningen tilrettelagt efter trefasemodellen dvs. intro, trænings- og studiefasen.

Introfase (forelæsning, holdtimer) - Antal timer: 24
Træningsfase: Antal timer: 36

Forelæsning vil fokusere på indførelsen af teoretiske modeller, programmeringssprog og relevante bevisteknikker.
Træningstimer vil fokusere på at få praktisk erfaring med disse værktøjer.

Studiefase vil bestå af følgende aktiviteter:

Læsning af skriftligt materiale tildelt af læreren.
Sammenligning af forskellige inference-baserede systemer.

Ansvarlig underviser

Navn	E-mail	Institut
Fabrizio Montesi	fmontesi@imada.sdu.dk	Concurrency

Skemaoplysninger

Odense

Vis fuldt skema

Administrationsenhed

Institut for Matematik og Datalogi (datalogi)

Team hos Registratur

NAT

Udbudssteder

Odense

Anbefalede studieforløb

Profil	Uddannelse	Semester	Udbuds periode

Overgangsordninger

Overgangsordninger beskriver, hvordan et kursus erstatter et andet kursus, når der ændres i et studieforløb.

Hvis der er lavet en overgangsordning for et kursus vil den fremgå af oversigten.
Se overgangsordninger for alle kurser på Det Naturvidenskabelige Fakultet.