Peter C. Ölveczky : Formal Modeling and Analysis of Distributed Systems in Maude, March 2010 . http://folk.uio.no/peterol/inf3230-lecturenotes.html.
Kompendiet selges ikke på Akademika (pga. problemer med Unipub/reprosentralen).
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.
English: The lecture notes ("book") given above are the main "textbook" for this course and are available on the web. The book is not sold at the bookstore.
As a rule, these lecture notes, as well as all the lectures, supplementary material, exercises with their solutions, and mandatory assignments define the core curriculum of the course. However, the footnotes and those parts of the course book that are explicitly marked as non-core reading are not required reading.
Kjernepensum/core curriculum
Essentially chapters 2 to 11 of the lecture notes (plus, in principle, lectures, exercises, etc.)
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.
Non-core curriculum/useful examples
Everything in the course that is not given as core curriculum or is explicitly removed from the curriculum, can be seen as "auxiliary" curriculum consisting of useful examples, discussions, etc. It is not necessary to have the same detailed knowledge of this part. At the same time, the course is essentially a course on modeling and analyzing distributed systems, for which these examples are useful. Examples of such examples include:
- "the sequence number (IP) protocol"
- the alternating bit and the sliding window protocols
- 2-phase-committal for distributed database systems
(That is, NSPK and its details are explcitly defined as core curriculum.)
Støttelitteratur/Supplementary resources
Filen prelude.maude leses inn automatisk av Maude og inneholder blant annet definisjonen av de innebygde modulene. Nyttig!
The file prelude.maude is read automatically by Maude and includes the definition of the built-in modules.
Maude-manualen anbefales for å lære mer om Maude og dens kommandoer.
The Maude manual is obviously a crucial resource.