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.
gøre rede for forskellige principper for automatisk verifikation.
anvende værktøjer til verifikation af tidslige egenskaber.
udnytte viden omkring verifikationsprincipper til valg af passende verifikationsparametre.
analysere afviklingsaspekter af tidstro systemer.
implementere tidstro 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. Modelleringsteknikker for hybride systemer. Specifikation og verifikation af tidslige egenskaber. Procesafvikling. Modellerings-, simulerings- og verifikationsværktøjer. Designprincipper. Implementeringsteknikker.
