At gøre deltagerne i stand til at konstruere sikre, tidstro computerbaserede systemer under brug af formelle modellerings- og verifikationsteknikker.
Læringsmål:
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
modellere sandtidssystemer ved brug af formelle modeller for tidslig opførsel.
formulere egenskaber for tidslig systemopførsel.
anvende værktøjer til verifikation af tidslige egenskaber.
udnytte viden omkring verifikationsprincipper i forbindelse med valg af passende verifikationsparametre.
analysere schedulerbarheden for en samling sandtidsopgaver.
foretage en udvælgelse af et passende scheduleringsprincip.
implementere sandtids-programmer på sandtids-operativsystemer.
anvende sandtidsbegreber til klar og præcis præsentation af problemer og løsninger.
Kursusindhold:
Højniveau modellering af tidslig opførsel. Specifikation og verifikation af tidslige egenskaber. Procesafvikling. Modellerings- og verifikationsværktøjer. Implementeringsteknikker.
