Professor: Luigi Logrippo
This document can be found on http://www.site.uottawa.ca/~luigi/csi5109
This course was taught for the last time in 2001. However these notes can still be useful since the basics of LOTOS theory have not changed.
This is a course on formal specification and verification of distributed systems (or reactive systems, as other people call them), based on algebraic and logical foundations. The LOTOS language will be the main reference topic, however hopefully you will learn much more than just LOTOS: purpose of the course is to teach the main ideas of this class of methods, which extends from CCS to CSP, to algebraic data types.
The basic structure of the course will be as follows (with possible variations from year to year).
By the end of the course, you should be able to understand the following topics:
Your understanding of these subjects should be sufficient to enable you to start studying the published literature.
The course subject has theoretical implications, which will be presented, therefore there will be some amount of formalism, definitions and proofs. However intuition and applications will be stressed over formality. The course is directed to students interested in studying this subject with emphasis on applications, rather than to students interested in the basic theory and its formal justification. I shall use examples from the area of telephone systems, protocols, and similar.
It is expected that you will do reading beyond the material presented in class, hence the list of references below.
Course notes available on-line:
Several people should be thanked for helping in the preparation of these notes: Jacques Sincennes formatted many figures, Bernard Stepien is the author of several examples in the initial chapters, students made suggestions for improvements. Unfortunately I can’t further improve the slides, because they were made in Frame, a system that I no longer have. Any errors will stay there…
Prerequisites for the course are a good background in computer science, and good understanding of formal reasoning, proof techniques, logic, automata theory, data communications protocols, and related areas (as usually possessed by students who have an undergraduate degree in Computer Science).
The course mark will be made of the following components:
(Do not let this marking scheme deceive you! Often students do very well in homework assignments, while it's the exam and report that bring the mark down).
Homework assignments are always due at the beginning of the following class. To help those people that may find it impossible to do all assignments in this specified time, if fewer than the required assignments are turned in, the remaining portion of the final mark will be taken from the average of the report and exam mark.
Homework assignments can be done in groups of two.
The exam will contain mostly questions similar to the ones of the homework assignments, although possibly not as lengthy. It will be a three-hour, open book exam, probably at the same time of classes one or two weeks after the end of the course.
The report will be on a subject of your choice. It it is not meant to be a substantial project, in particular it is not meant to have a programming component (although something of this type could also be done, if you wish). It must be related to the course content, although it could go well beyond it. A typical report may be centered around one or two substantial papers in the course's research area, and present your understading of the subject. For example, it might include some additional examples showing your insight in the subject matter, discuss an application, relate the main paper to other similar ones, etc. Typically, you may choose to write a survey-type paper. In such a paper, I shall be looking for plenty of citations, since the number of citations provided will probably be a good indication of the extent of your research. Or you may decide to write a monographic paper on a specific item. In such a paper, I shall be looking for several good examples (beyond those discussed in your sources) and interesting insight on your source material. Or you may write a tool paper, involving experimentation with existing LOTOS software tools on specifications written by you or found in the literature. This may involve analyzing in depth one or more existing nontrivial specifications, writing your own specification and discussing its design, validity, etc., by using existing tools. Finding your topic is part of learning: you will have to do reading and learning as you try to find a suitable subject. Length should be in the order of 25 pages, but this is highly individual because much depends on the the space taken by figures, page layout, difficulty of topic, etc. The QUALITY of your writing will be much more important than its QUANTITY! Also, your personal touch on the subject is essential, otherwise it will look like straight regurgitation, or like a copy job (in this respect, it is very important that you respect guidelines to avoid plagiarism). Of course, you will use word-processing. Please include your coordinates on the title page (phone numbers, email) because I may wish to get in touch with you for questions on your work.
The report will be judged according to the following criteria:
As soon as you choose your topic, you should write maybe a page for the professor, outlining what you are planning to do. Ideally, this should be done within the first five weeks of classes. A preliminary report of about 5-10 pages should be submitted within the first ten weeks. These preliminary reports are not compulsory and are not marked, but will allow you to obtain some preliminary feedback on the direction of your work. Depending on the number of students in the course, you may be asked to give a short presentation, probably in the last week of the course.
Report due date will be around exam time. This will be discussed further during course.
Reports should be submitted by email in some commonly known electronic format, such as postscript, Word or pdf. Please avoid bulky files including fancy figures that take space and won't impress me much.
I should mention that every year I get some reports that are sound technically, and also embody the result of a good amount of reading, but which however I find disappointing. This is usually because the student has just lifted text from the literature, perhaps even organizing it well, but without adding the necessary personal touch in the form of additional explanations, examples, remarks, etc. Or because the student has tried to impress the reader by including a tangle of complicated technicalities, without sufficient explanations or examples. Or because the student has failed to make appropriate reference to her sources. It is also important that student discusses with professor the report content, and that she follows up on professor's suggestions. Some students do not do that, and simply present the professor with a finished paper on the deadline. Such students risk a low mark because it may not be clear if the work is really theirs or if they have just copied it from somewhere. In other words, make sure that professor knows what you are doing, and that he knows how much you have learned.
Following is a list of some papers and books related to course contents. This is an uneven list. Some of these are old classics, others are just papers that I found interesting and you might find interesting as well. Much important material in this area is still buried in conference proceedings and hard-to access sources. Some important concepts have not yet been explained well for general consumption.
Abramski, S., Gabbay, D.V., and Maibaum, T.S.E.
Handbook of Logic in
A Survey of Verification Techniques for Parallel Programs. Lecture Notes in Computer Science, No. 191. Springer, 1985. QA 76.L42 v.191 1985
Bergstra, J.A., Heering, J. and Klint, P.
Algebraic Specification. 1989. QA 76.9.A23 A44 1989
Berztiss, A.T., and Thatte, S.
Implementation of Abstract Data Types. In: Advances in Computers, Vol 22 (Ed.
M.C. Yovits), Academic Press,
* Bolognesi, T., van de Lagemaat, J., and Vissers, C.
LOTOSphere: Software Development with LOTOS. Kluwer Academic Publishers, 1995. QA 76.73 .L65 L68 1995
Distributed Systems Analysis with CCS. Prentice-Hall, 1997. QA 76.9 .D5 B78 1997
The OSI95 Transport Service with Multimedia Support. Springer, 1994. TK 5105.55 .O85 1994 (includes specification in LOTOS of broadband protocols).
Ehrig, H., and Mahr, B.
Fundamentals of Algebraic Specification 1. Springer-Verlag 1985. QA 76.9.D35 E37 1985.
Introduction to Process Algebra. Springer, 1999
Goguen, J. and Malcom, G.
Algebraic Semantics of Imperative Programs. MIT Press, 1996.
Guttag, J.V., Horowitz, E., and Musser, D.
The Design of Data Type Specifications. Current Trends in Programming Methodology. ed. R. Yeh, Vol.IV, Prentice-Hall, 1978. (this book, as well as vol. I of the same series, contains other papers of interest). QA 76.6.C87
Hailpern, Brent T.
Verifying Concurrent Processes Using Temporal Logic. Lecture Notes in Computer Science No. 129 QA 76.L42
Hailpern, B.T., and Owicki, S.S.
Modular Verification of Computer Communication Protocols. IEEE Trans. on Comm. Vol. COM-31 (Jan. 1983) 56-68.
Algebraic Theory of
The Semantics of Programming Languages. Wiley, 1990. QA 76.7.H45 1990.
Hinchey, M.G. and
Concurrent Systems: Formal Development in CSP. McGraw-Hill, 1995.
* Hoare, C.A.R.
Communicating Sequential Processes. Prentice-Hall, 1986. QA.76.6.H57 1985
Temporal Logic of Programs. Springer-Verlag, 1987. QA 76.6.K753 1987.
Liskov, B., and Zilles, S.
An Introduction to Formal Specification of Data Abstractions. In: R. Yeh (ed.) Current Trends in Programming Methodology, Vol. 1, 1-32. QA 76.6.C87
Manna, Z. and Pnueli, A.
The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, vol. 1 and 2, 1992 and 1995. QA 76.6 .M3573
Meseguer, J., and Goguen, J.A.
Initiality, Induction, and
Computability. In: M.Nivat and J.C.Reynolds (eds.) Algebraic Methods in
A Calculus of Communicating Systems. Lecture Notes in Computer Science, No. 92. Springer-Verlag 1980. QA 76.L42 v.92 1980
* Milner, R.
Communication and Concurrency. Prentice-Hall, 1989. QA267.M533 1989
Elements of Interaction (Turing Award Lecture). Comm. ACM, Vol. 36, No 1, 78-89.
The Theory and Practice of Concurrency. Prentice-Hall, 1998
Principles of protocol engineering and conformance testing. Ellis Horwood, 1993. TK 5105.5 .S265 1993
* Turner, K.J. (Ed.)
Using Formal Description Techniques. An Introduction to Estelle, LOTOS and SDL. Wiley, 1993. QA 76.6.U848 1993
* van Eijk, P.H.J., Vissers,
The Formal Description Technique LOTOS. North-Holland, 1989. QA 76.9.D5 F65 1989
van Leeuwen, J. (ed.)
Handbook of Theoretical Computer Science. Volume B: Formal Models and Semantics. MIT Press/Elsevier, 1990. QA 76.H279 1990 v.B. See esp. Chapter 6 (Dershowitz and Jouannaud: Rewrite Systems), Chapter 13 (Wirsing: Algebraic Specifications), Chapter 16 (Emerson: Temporal and Modal Logic), Chapter 18 (Lamport and Lynch: Distributed Computing, Models and Methods), Chapter 19 (Milner: Operational and Algebraic Semantics of Concurrent Processes).
This is just a start: you will find many additional references in these papers and books. There is a whole world out there, waiting to be discovered by you! If you find a good book that is not mentioned above, let me know. Periodicals that regularly include articles related to the subject matter of this course are: The yearly series of books Protocol Specification, Testing, and Verification and Formal Description Techniques, both published by North-Holland, the journal Computer Networks and ISDN Systems, the Lecture Notes in Computer Science, the IEEE Transactions on Software Engineering, the ACM Transactions on Programming Languages and Systems.
When borrowing books, please be considerate to others. Use photocopying and
keep the books for as short a time as possible. Obviously a few of you could
sabotage the learning of others just by borrowing as many books as possible and
keeping them for as long as possible. Remember that there are several good
libraries in town (for example, Carleton U and CISTI on
Starred books will be put on reserve at the library. I may also put on reserve some other materials.