Peter C. ?lveczky : Formal Modeling and Analysis of Distributed Systems in Maude, April 2008. http://folk.uio.no/peterol/inf3230-lecturenotes.html.
Siden Unipub/reprosentralen har hatt en historie for ? trykke opp uleselige kompendier, og for ? rote til mye p? andre m?ter, s? vil kompendiet ikke selges p? Akademika. Jeg planlegger ? dele ut de f?rste kapitlene p? f?rste forelesning, mens hele kompendiet vil ligge p? web.
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.
Det fins ogs? en "primer" om Maude her .
Here is a "Maude primer".