Course CSI 5109 (95.571) - Specification Methods for Distributed Systems

Professor: Luigi Logrippo

luigi@site.uottawa.ca

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.

Course Contents

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).

  1. Principles of specifying and verifying distributed systems.
  2. Basic LOTOS. Equivalence relations between behavior expressions.
  3. Testing theory.
  4. Verification of recursive programs. Structural induction.
  5. Algebraic Abstract Data Type Specifications and Rewriting Systems. Proof principles.
  6. Full LOTOS.
  7. Concepts of Specification Style.
  8. Relation with other algebraic models: CCS, CSP.
  9. Relation with temporal logic.
  10. Report presentations.

By the end of the course, you should be able to understand the following topics:

  • how reactive or distributed systems can be described precisely
  • how such systems can be proved correct
  • the concept of behavioral equivalence
  • the basis of formal specification languages such as LOTOS, CCS, CSP
  • principles of data type specification, verification of data types
  • principles of formal testing based on these concepts

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.

Handouts, Books, Reserve

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

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).

Marking Scheme

The course mark will be made of the following components:

  • 33% Homework Assignments (Roughly a set every second week). Can be done in groups of two.
  • 33% Final Exam. 3 Hours, Open Book.
  • 33% Report

(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

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.

Exam

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.

Report

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:

  • Clarity of explanation (the professor has not necessarily read the paper(s) you are reporting on, so it is very important that the discussion be self-contained; the only concepts you can assume are those covered in the course).
  • Depth of research
  • Student's own insight.
  • Responsiveness to professor's suggestions on preliminary discussions and preliminary drafts.

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.

References

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 Computer Science. Oxford Science Publications, 1992. QA 76 .H2785 1992

Baeten, J.C.M.

 Process algebra. Cambridge University Press, 1990. QA 267.B33. 1990

Barringer, H.

 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.

 Specification and Implementation of Abstract Data Types. In: Advances in Computers, Vol 22 (Ed. M.C. Yovits), Academic Press, New York, 1983. SC QA 76.A39

* Bolognesi, T., van de Lagemaat, J., and Vissers, C.

 LOTOSphere: Software Development with LOTOS. Kluwer Academic Publishers, 1995. QA 76.73 .L65 L68 1995

Bruns, G.

Distributed Systems Analysis with CCS. Prentice-Hall, 1997. QA 76.9 .D5 B78 1997

Danthine, A.

 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.

Fokkink, W.

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.

Hennessy, M.

 Algebraic Theory of Processes. Cambridge, 1988. QA 76.9.M35 H46 1988.

Hennessy, M.

 The Semantics of Programming Languages. Wiley, 1990. QA 76.7.H45 1990.

Hinchey, M.G. and Jarvis, S.A.

 Concurrent Systems: Formal Development in CSP. McGraw-Hill, 1995.

* Hoare, C.A.R.

 Communicating Sequential Processes. Prentice-Hall, 1986. QA.76.6.H57 1985

Kroger, F.

 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 Semantics. Cambridge University Press, 1985, 459-541. (this book contains other articles of interest). QA 76.7.A43 1985

Milner, R.

 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

Milner, R.

 Elements of Interaction (Turing Award Lecture). Comm. ACM, Vol. 36, No 1, 78-89.

Roscoe, A.W.

The Theory and Practice of Concurrency. Prentice-Hall, 1998

Sarikaya, B.

 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, C.A., Diaz, M. (eds.)

 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 Montreal Road). It might be worthwile to visit these and to use interlibrary loans.

Starred books will be put on reserve at the library. I may also put on reserve some other materials.

Electronic sources

  • http://www.site.uottawa.ca/~lotos/ is the web site of the University of Ottawa LOTOS group, now inactive. Many links, materials and references can be found here.
  • One of the most informative sites for LOTOS research is the WELL (World Environment for Learning LOTOS) site maintained by Ken Turner in Scotland.
  • LOTOS is alive and well in the project VASY at INRIA, France. This site distributes the LOTOS toolkit CADP that is in use in many research groups. It also maintains a LOTOS discussion group.