Peter C. ?lveczky : Formal Modeling and Analysis of Distributed Systems in Maude, 2005. Kompendiet p? pdf-format.
Som hovedregel er kompendiet, alle forelesninger med foiler, ukeoppgaver med l?sningsforslag og obligatoriske oppgaver pensum.
Fra kompendiet utg?r fotnoter og de markerte "ikke-pensum" delene. I tillegg er ikke Avsnitt 4.2 ('Inductive Theorems') pensum.
Kjernepensum: alt som er nevnt over er pensum, men f?lgende er en grei definisjon av hva som skulle dekke mesteparten av kjernepensum:
- kapitlene 2-8 og 11 fra kompendiet
- unntak: alt i kompendiet som er merket som "ikke pensum" (ved innrykk etc. som forklart i introduksjonen)
- forelesning 13 om temporale egenskaper og s?rlig invarianter
- oppgavesett 14 med l?sningsforslag, om invarianter.
Kursorisk pensum og nyttige eksempler
Alt annet som ikke er markert i punktet over, eller som eksplisitt er fjernet, er kursorisk pensum som er gode eksempler, diskusjoner etc. Det er ikke n?dvendig ? ha samme detaljkjennskap til kursorisk pensum som til kjernepensum. Samtidig er mye av kurset en trening i ? modellere og analysere distribuerte systemer, s? disse eksemplene gir masse nyttig trening i det. Kursorisk er s?rlig:
- "sekvensnummer-protokollen"
- alternating bit protocol og sliding window-protokollen
- 2-fase-committal protokollen for distribuerte databaser.
I tillegg er forelesningene, ukeoppgavene, obligatoriske oppgaver, og eventuelle andre notater som deles ut p? forelesning eller finnes p? kursets hjemmeside ogs? pensum.
St?ttelitteratur
Filen prelude.maude leses inn automatisk av Maude og inneholder blant annet definisjonen av de innebygde modulene. Nyttig!
Maude-manualen anbefales for ? l?re mer om Maude og dens kommandoer.
Det fins ogs? en "primer" om Maude her .