Formal Methods 2

Emnet undervises annet hvert år, neste gang vår 2016. Emnet fordyper og utvider metoder og teori fra TM8103 Formelle Metoder i selvstudier. Spesielt vuderes metoder for utvikling av korrekt programvare med hjelp av temporallogik.

A. Kunnskap: 1) En god innsikt i muligheter, metoder og utfordringer innen formal modellering, verifikasjon og utvikling av funksjonale egenskaper i informasjon- og kommunikasjons-teknologiske (IKT) systemer baser på Temporal Logic of Actions (TLA) og compositonal TLA (cTLA). 2) Dybdekunnskap på å beherske de forskjellige tekniske fremgangsmåtene å spesifisere systemer i temporallogikk og å lagre raffineringsbevis at en mer detaljert oppfyller en mer abstrakt systemspesifikasjon. 3) Basiskunnskap om verifiseringsverktøy som TLC. B. Ferdigheter: 1) Beherske terminologi og begrepsdannelse innen området av temporallogikk. 2) Kunne spesifisere modeller for IKT systemer i cTLA. 3) Beherske verifikasjon av både invariante system egenskaper og raffineringsbeviser. C. Generell kompetanse: 1) Bedret innsyn i fordelene av systemutvikling basert på temporallogikk sammenliknet med andere formale modeleringsmetoder.

Ledet selvstudium. Karakterregel er bestått/ikke bestått, hvor en fastsatt poenggrense 70/100 poeng (70%) gir kandidaten karakter bestått.