Beskjeder
Modellsjekkeren SPIN:
Vi benytter Spin til modellsjekking. Den er lagt opp p? linuxsystemet p? ifi. Det grafiske grensesnittet Xspin er ogs? tilgjengelig. Hvis dere ikke f?r det opp direkte ved "xspin", kan dere pr?ve "wish /store/bin/xspin".
Det kan v?re greit ? se litt p? systemet f?r dere f?r ny oblig... Noen oppgaver for ? sette seg inn i Spin, finner dere her . Dessuten: Eratostenes Sil og AB-protokollen .
PROMELA
Programmer/modeller til Spin skrives i Promela. En kort introduksjon til Promela finner du her . Mer informasjon om Spin og tutorials finnes p? Spin's hjemmeside .
Forelesningen i p?skeuka utg?r (p? foresp?rsel). Jfr. oppdatert forelesningsplan.
Jeg har lagt opp til et par uker med selvstudium i forbindelse med obligatorisk innleveringsoppgave. Det er mulig ? organisere en slags kollokvie siste uken f?r innlevering (dvs. 16 mars), hvis dere ?nsker det.
I morgen tar vi et tilbakeblikk p? slutningsregler og resonnering rundt programmer for de som ikke er kjent med det. Essensielt ser vi p? kap. 2 fra Andrew's bok (fra pensum i INF3140, deles ut p? forelesning) og ser p? noen eksempler. Dette er ikke direkte pensum i INF5140. Vi fortsetter med transisjonssystemer og temporallogikk om en uke.
Det er obligatorisk fremm?te p? f?rste forelesning. Hvis du ikke m?ter eller ikke har f?tt fritak for fremm?te f?r forelesningen, s? mister du plassen p? emnet.
Etteranmelding til emner som eventuelt har ledig kapasitet, kan skje tidligst dagen etter f?rste forelesning i det aktuelle emnet. Opptak gj?res deretter fortl?pende frem til emnet er fullt.
-Studieadministrasjonen