Faglig innhold

Kurset dreier seg om programvareutviklingsprosessen for pålitelige og sikkerhetskritiske distribuerte reaktive systemer. Spesielt lærer studentene hvordan man kan lage slike systemer med abstrakte systemmodeller som utgangspunkt via designsyntese til kodegenerering og eksekvering. I tillegg bruker vi den relativ enkle formelle modelleringsteknikk Temporal Logic of Actions (TLA) og sitt programmeringsspråk TLA+ til å spesifisere sikkerhetskritiske systemer. I tillegg vil modellkontrolleren TLC brukes til å automatisk verifisere at utviklingen av mer detaljerte systemer basert på mer abstrakte systemmodeller er korrekt og at spesifiske sikkerhetskritiske egenskaper er garantert. Til slutt diskuterer vi hvordan sikre systemer kan testes skikkelig.

Kurset består av de følgende enhetene:

Enhet 1: Implementering av tilstandsmaskiner (SM)

• Introduksjon til utvikling av sikkerhetskritiske systemer.
• Få en oversikt over modellering av slike systemer.
• Oppfrisk kunnskapen din om tilstandsmaskiners semantikk, og hvordan tilstandsmaskiner kan implementeres i kode.

Enhet 2: Systemarkitektur og standardisert utvikling

• Få en forståelse av hvordan redundans, pålitelighet og tilgjengelighet påvirker sikkerheten til et system.
• Forutsi feilfrekvenser i 2oo3- og 2oo4-systemer.
• Overholdelse av sikkerhetskriterier og standarder.

Enhet 3: Mot temporal logikk: Notasjonen TLA+

• Få en forståelse av hvordan man realiserer tilstandsmaskiner ved hjelp av notasjonen TLA+.
• Lær å lage enkle spesifikasjoner i TLA+.
• Utfør de første bevisene på egenskaper ved hjelp av modellkontrolleren TLC.

Enhet 4: Tidslogikk for handlinger (TLA)

• Forstå tidsformler og forskjellen mellom sikkerhet og livskraft.
• Lær å spesifisere og verifisere at en spesifikasjon er en videreutvikling av en annen (trinnvise videreutviklinger).
• Gjennomfør trinnvise videreutviklingsbevis med TLC.

Enhet 5: Kvalifisering av sikkerhetssystemprogramvare

• Få en oversikt over prosessen med lisensiering av programvare.
• Verifiserings- og valideringsprosessen for kvalifisering av programvare.
• Design et større eksempel på et sikkerhetskritisk system ved hjelp av metodene du har lært i kurset.

Enhet 6: Testing

• Lær om de viktigste ideene og teknikkene for testing av systemer.

Læringsutbytte

A. Kunnskap:

1. Programvareutviklingsprosess for sikkerhetskritiske systemer.
2. Modelbaserte utviklingsmetoder til å lagre pålitelige og sikkerhetskritiske distribuerte reaktive systemer fra abstrakte systemmodeller via designsyntese til kodegenerering og eksekvering.
3. Formelle spesifikasjon av sikkerhetskritiske systemer i en lett forståelig temporallogikk og automatiske verifikasjon av systemegenskaper med modellsjekkere.
4. Systemvalidering gjennom testing.

B. Ferdigheter:

1. Bruk av utvalgte UML-baserte modelleringspråk, metoder og verktøy for spesifikasjon, design, implementering og analyse av sikkerhetskritiske systemer.
2. Bruk av spesifikasjonsspråket TLA+ for å modellere systematferd. TLA+ er basert på Temporal Logic of Actions (TLA) og gjør det mulig å modellere systemer ganske lik programerspråk.
3. Bruk av modellsjekkeren TLC som er også basert på TLA å garantere at systemmodellene oppfyller visse sikkerhetskritiske egenskaper og at et mer detailert system faktisk implementerer et mer abstrakt system.
4. Praktisk utvikling og eksekvering av pålitelige systemer som følger den generelle programvareutviklingsprosessen for sikkerhetskritiske systemer.

C. Generell kompetanse:

1. Anvendelse av prinsippene for programvaredesign av distribuerte sikkerhetskritiske systemer.
2. Grunnleggende forståelse for bruk av formelle metoder til å spesifisere og verifisere sentrale egenskaper av pålitelige systemer.

Læringsutbyttet av dette kurset er knyttet til konstruksjon av sikkerhetskritiske systemer som vil bli ryggraden for digitale økosystem, dvs. integrerte distribuerte systemer og andre kritiske infrastrukturer. Slike systemer er viktig for samfunnet og må derfor implementere funksjoner på en robust, sikker og effektiv måte. Derfor er utbyttet av dette kurset direkte relatert til FNs bærekraftsmål (SDG) 9 (Industri, innovasjon og infrastruktur). Indirekte hjelper vunnet kunnskap, ferdigheter og kompetanse også i hensikt til andre bærekraftsmål som muliggjørende teknologi i ulike områder, særlig mål 2 (Utrydde sult), 3 (God helse og livskvalitet), 7 (Ren energi til alle) og 11 (Bærekraftige byer og lokalsamfunn).

Læringsformer og aktiviteter

Kurset blir undervist etter prinsippet av team-basert læring. Opplegget består individuell læring, gruppearbeid og forløpende tilbakemelding. Hensikten er at studenter skal delta mer aktivt i kurset. Prinsippet er forklart på www.teambasedlearning.org. Gjennom semesteret får studentene tilbakemelding på læringsfremgang gjennom flere tester (Readiness Assurance Tests (RATs)), som også teller til sluttkarakter. For å kunne gå opp til eksamen må en student klare minst 40% av poengene i readiness assurance testene.

Anbefalte forkunnskaper

TTM4115 Design av kommuniserende systemer eller tilsvarende forkunnskaper.

Kursmateriell

I dette emnet benyttes to hovedressurser:

1. Development of Safety-Critical Systems av Gopinath Karmakar, Amol Wakankar, Ashutosh Kabra og Paritosh Pandya, tilgjengelig som e-bok via NTNUs nettverk; og
2. TLA+ videokurset av Leslie Lamport, som er fritt tilgjengelig på nett.

Studiepoengreduksjon