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 tidstro systemer 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.
forstå udvalgte verifikationsteknikker samt kende deres fordele
og begrænsninger.
at benytte forskellige abstraktionsniveauer under udvikling af
tidstro systemer.
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.
