Velkommen til IN2100
Hva er poenget med IN2100?
Poenget med emnet er ? modellere og analysere distribuerte datasystemer. Distribuerte systemer er systemer hvor flere noder/maskiner 澳门葡京手机版app下载er for ? f? til noe, typisk ved ? sende meldinger. Alle dagens st?rre datasystemer er distribuerte systemer. ? ?
Det viser seg at det er veldig mye vanskeligere ? forst? og designe distribuerte systemer enn vanlige "sekvensielle" systemer. Akkurat som en arkitekt lager modeller av st?rre bygninger f?r man begynner ? bygge dem, og analyserer modellene f?r bygging, p? samme m?te m? vi f?rst designe og modellere et komplekst datasystem, *f?r* designet implementeres. Det er design av slike systemer som er vanskelig; ikke ? implementere dem. Men for at et design skal kunne analyseres p? en seri?s m?te, m? det v?re en klar og éntydig modell, og det m? finnes analysemetoder som lar oss analysere et design (i stedet for ? bare ni-stirre p? et designdokument). Modellen m? derfor v?re en matematisk modell. P? den m?ten kan vi bruke datamaskiner til ? analysere modellen matematisk, for ? finne feil s? tidlig som mulig i systemutviklingsprosessen. Akkurat som arkitekten bruker sin modell (og matematiske regler og fysiske lover) til ? beregne hvorvidt en bro vil kollapse, lenge f?r man setter i gang med ? bygge broen.
Vi bruker det funksjonelle spr?ket Maude (https://maude.cs.illinois.edu) til ? lage modeller av distribuerte systemer, og til ? analysere v?re design p? ulike m?ter. Maude er b?de et modelleringsspr?k og et "funksjonelt" programmeringsspr?k, s? man kan si at vi programmerer (design til) distribuerte systemer.
Et annet m?l med emnet er ogs? ? gi en innf?ring (og intuisjon) rundt distribuerte systemer, som muligens er en mangelvare p? (lavere grad?) p? Ifi. Emner vil derfor introdusere (og modellere) helt sentrale algoritmer/protokoller for distribuerte systemer, som brukes i dagens systemer. Kommunikasjonsprotokoller som TCP, alternating bit protocol, og sliding windows; distribuerte algoritmer som to-fase commit, distribuerte protokoller for gjensidig utelukkelse ("mutual exclusion"), valg av leder, osv. Vi skal ogs? modellere og knekke en klassisk sikkerhetsprotokoll. Disse metodene har v?rt brukt av mine venner til ? knekke betalingssystemere til VISA og MasterCard, som vist i vidoen
https://www.vgtv.no/video/205022/ny-svindelmetode-slik-kan-de-kopiere-kortet-ditt-i-koeen.
En av de tre som knekket VISA/MasterCard pleier normalt ? holde en forelesning om dette; jeg h?per det er tilfelle ogs? i ?r. Emnet vil ogs? omhandle bruk av Maude p? st?rre cloud-baserte transaksjonsstymer, og vil diskutere bruk av formelle metoder hos Amazon Web Services.
Innhold:
Vi m? l?re oss modelleringsspr?ket Maude for ? kunne modellere distribuerte systemer i Maude. De f?rste ukene starter vi derfor med ? modellere enkle datatyper og diverse funksjoner p? slike, ved ? bruke funksjonell programmering. Vi programmerer ymse funksjoner p? lister og mengder, osv. Sorteringsalgoritmer som quick-sort, merge-sort, osv., og NP-komplette problemer som Subset Sum og Traveling Salesman.
Deretter f?lger tre teoretiske uker, hvor vi bruker matematiske/logiske metoder til ? resonnere om terminering, konfluens, og likhetslogikk.
Etter de tre ukene begynner vi med distribuerte systemer, og vil modellere systemene beskrevet ovenfor. Vi avslutter med ? introdusere temporallogikk for ? spesifisere krav til distribuerte systemer, og bruker Maude for ? sjekke hvorvidt et design tilfredsstiller ?nskede krav.
Forh?ndskunnskaper:
Strengt tatt ingenting. Jeg antar at man kan programmere, f eks at man har tatt basale/obligatoriske programmeringsemner p? Ifi. Ellers vil jeg introdusere det man trenger av matematikk, som essensielt er "hva er en funksjon?", "hva er en (bin?r) relasjon?", og "hva er en partiell ordning?". Det er sikkert en fordel ? ha hatt litt logikk, a la IN1150, men dette er ikke n?dvendig. Siden funksjonell programmering "bygger p?" rekursjon, er det fint hvis man lagd noen rekursive prosedyrer/metoder/funksjoner.
Samtidig er dette et universitetsemne, slik at man kan forvente en viss modenhet og evne til abstrakt/logisk/matematisk tenking. Det er ingen matematisk analyse, derivering, eller lignende matematikk i emnet. Det er typisk de tre "teoretiske" forelesningene tidlig i emnet som kanskje setter krav til litt tenkning.
Jeg antar absolutt ingen kjennskap til distribuerte systemer, som operativsystemer, kryprografiske protokoller, nettverk, eller andre typer distribuerte systemer. De vil introduseres i emnet.
Pensum-materiale:
Pensum er essensielt l?reboken "Designing Reliable Distributed Systems", skrevet av meg. Den finnes kun i én utgave, og er normalt ? f? kj?pt i bokhandelen p? Frederikke. Den er ogs? tilgjengelig (gratis) fra UiO-nettet. I tillegg er artikkelen "How Amazon Web Services Uses Formal Methods," skrevet av ingeni?rer p? AWS som utviklet store sentrale systemer for AWS, pensum. I tillegg er som vanlig alle forelesningene, ukeoppgavene, og s? videre, pensum.
Arbeidsmengde:
10 studiepoeng skal tilsvare 13-14 timer arbeid i uka. Hvis man f?lger forelesninger og gruppetimer, b?r man alts? bruke 9-10 timer i uken p? eget arbeid med emnet. I s?rdeleshet er det ?nskelig at man har jobbet med ukeoppgavene f?r man kommer p? gruppetimer.
Eksamen:
Man kan ha med seg l?reboken og det man ?nsker av skriftlig materiale til eksamen.