Sesjonstyper

Sesjonstyper er et type-system som beskriver kommunikasjonen mellom prosesser i et distribuert system. De uttrykker hvilke meldinger som kan utveksles, i hvilken rekkefølge, og under hvilke betingelser. Målet er å sikre at klienter og tjenester følger en angitt protokoll, og dermed oppdage feil i kommunikasjonen tidlig gjennom statisk analyse.

En sesjonstype beskriver en kanal som en sekvens av operasjoner, for eksempel utgående sending (!T) og innkommende mottak (?T), samt en avslutning End. For to parter er typene duale: det som kan sendes av den ene part, må kunne mottas av den andre.

Avanserte varianter inkluderer rekursive typer for uendelige protokoller og valg/branches for situasjoner med betinget kontrollflyt. Multiparty session types (MPST) beskriver protokoller mellom flere parter ved hjelp av globale typer, som senere projiseres til lokale typer for hver deltaker.

Eksempel: En enkel klient–server-protokoll kan beskrives som klienten følger !Request . ?Response . End, mens serveren følger ?Request . !Response . End.

Bruk og begrensninger: Sesjonstyper brukes i formelle språk og verktøy for å sikre kommunikasjonssikkerhet, deadlock-freedom og protokollkonsistens. De gir betingelser som er nyttige for verifikasjon av distribuerte systemer, men implementering kan være kompleks, og støtte i programmeringsspråk varierer.