Enkeltfag Engelsk 5 ECTS

Formelle aspekter af process science

Overordnede kursusmål

Kurset giver en omfattende oversigt over standard og moderne tilgange til ræsonnering om processer i informationssystemer. Disse processer varierer i kompleksitet, fra e-handelsarbejdsgange til sikkerhedskritiske sundhedssystemer. Gennem kurset opnår de studerende dybdegående viden om formelle modelleringsnotationer (baseret på Petri-net og temporale logikker) og relaterede analyseteknikker, efterfulgt af grundige studier af praktiske anvendelser. Derudover får de studerende mulighed for at eksperimentere med forskellige design- og analyseværktøjer til det formalismestudie, der dækkes i kurset, samt udvikle deres egne modellerings- og analyseværktøjer baseret på den viden, de tilegner sig undervejs.

See course description in English

Forklar syntaks og eksekveringssemantik for flere klasser af Petri-net.
Forklar syntaks og semantik for flere temporale logikker.
Forklar, hvordan temporale logikker kan bruges til modellering og specifikation af procesegenskaber.
Identificér Petri-net-klasser og brug dem til at oprette modeller for et givet scenarie.
Identificér deklarative formaliser og brug dem til at oprette modeller for et givet scenarie.
Forklar, hvordan forskellige beregningsmodeller (rækkevidde- og dækbarhedsgrafer) kan genereres fra Petri-net ved hjælp af deres eksekveringssemantik.
Forklar de algoritmiske aspekter af analyseteknikker, der er blevet studeret i kurset.
Argumentér formelt for, hvorfor et givet Petri-net eller deklarativ model har visse egenskaber.
Betjen modellerings- og verifikationsværktøjer og fortolk deres resultater.
Kobl tilgange og koncepter fra relevant litteratur til dem, der er blevet gennemgået i kurset.
Opret procesmodelleringsformalismer, definer deres formelle egenskaber og udvikl værktøjsunderstøttelse.

Kurset vil dække følgende emner:
● Klasser af Petri-net og deres udvidelser med data, tid og stokastiske egenskaber. Strukturelle og adfærdsmæssige egenskaber ved disse klasser; afgørelsesresultater for centrale analyseteknikker såsom begrænsning, rækkevidde, dækbarhed og terminering. Verifikation af disse Petri-net-klasser ved hjælp af temporale logikker.

● Grundlag for deklarative procesmodeller baseret på Lineær Temporal Logik på endelige spor og dens førsteordensudvidelser. Analyse af deklarative processer i forbindelse med modeltjek, runtime-verifikation/overvågning og tilfredsstillelse.

● Softwareværktøjer til analyse og modellering af Petri-net og deklarative processer baseret på temporale logikker.

36 – 49 (man 8-12)

02141, De studerende forventes at være fortrolige med endelige automater og/eller transitionssystemer. De studerende skal være i stand til at skrive programmer i et programmeringssprog.

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