The aim of this one-week appetizer to topics in the field of Operating
Systems is to introduce you to some of the basic concepts and
algorithms from that area of Computer Science that you will find most
useful in your studies of control software and systems.
During the course, you will learn about topics such as:
Since concurrent programming is notoriously tricky, we will use these
topics as an excuse to introduce you to some of the techniques and
tools of model-based development of concurrent, reactive systems, of
which control programs are one of the many examples. We hope that,
after having met these techniques and tools in this course, you will
be enticed to use them throughout your careers in building
high-quality systems from models, which you have previously subjected
to thorough automated analysis.
Slides for the course (also available from the MySchool pages for
the course, from where audio files for lectures on processes are also
available). Note! These slides are still in draft form
and are only posted here for early reference!
Activities: Install Uppaal on your machines.
Start reading the Tutorial
on Uppaal and the on-line help, ignoring the aspects having to do with real-time,
and, most importantly, start playing with the tool! Draw some automata and ask the tool
questions about their possible behaviour.
To get started, you may download and play with the
example from the The Little Book of
Semaphores by Allen B. Downey. A version without early deadlocks is available
Try to make models of some concurrent programs. For instance, you might immediately get
started on your project work. (See the suggested activities for Tuesday and Wednesday.)
Tuesday-Wednesday, 27-28 November 2007. (Independent work sessions) Lecturers: None.
Topic: The joys
of concurrency Reading material:
Activities: Work on the project assignment. You should model and verify the roller coaster
problem on pages 153-158 of The Little Book of
Semaphores by Allen B. Downey. You can assume that there are 3 passenger processes and that the car holds 2 passengers.
Make sure you finish the project work having to do with mutual exclusion algorithms!
Friday, 30 November 2007, from 8:30 till 10:15.
Lecturer: Luca Aceto.
Topic: Deadlock Reading material:
Activities: Work on the project assignment. You should model and verify the unisex bathroom
problem on pages 170-173 of The Little Book of
Semaphores by Allen B. Downey. You can assume that there are two women
and three men using the toilet.
Your work during this week will be evaluated based on a group project,
which is due on Sunday, 2 December 2007, at 23:59 GMT. We
suggest that you work on the project in groups of three-four
students. Your project report must be in pdf format, and is expected to contain clear, concise and polished descriptions
of your solutions to the problems mentioned above and
of your experiences in working with Uppaal.
Your project report should be no longer than 10 pages.
Last modified: 25 November 2007