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.
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.
