CS615 Course Project Information (Autumn 2006)

For your CS615 course project, you are required to work in groups of two. Two groups have taken special permission so far for working in groups of three, but all other groups should be of size two. If you need to work in a larger group, please contact the instructor/TA asap.

The project will involve modeling a system of your choice and identifying some interesting properties to be checked of this system. In consultation with the instructor and/or the TA, you are then required to choose a tool for checking these properties of the system. We wish to emphasize again that you must choose a system that is from your domain of interest for the verification project. The tool to be used for verification will be based on the type of system you choose to verify and on the capabilities of different tools available. The tool must be chosen in consultation with the instructor and/or the TA. You must not choose the tool arbitrarily. Also, you must not choose a tool and then choose a system that fits within the capabilities of the tool. The purpose of the project is to give all of you some experience of modeling a system,specifying its properties and then actually verifying these properties. So the focus is on the process of verification and not on the tool. Hence, you cannot choose the tool to begin with. The tool must be chosen once you have identified a system of small enough size to attempt verification.

We've received several queries about the kind of systems that should be chosen for verification. Well, this is your and your group partners' responsibility. We would like each group to come up with a suggestion of a system and some example properties that would be interesting to check. This system could be something that you find interesting, or you think is a tricky one to verify, or something that is just in your specific area of liking within CS.

Of course, one needs to be careful when choosing the size and complexity of the system to be verified. For example, if you say that you want to check that the Linux operating system can never be made to deadlock, that's a formidable challenge. In order to give you an idea of the size and complexity that can be reasonably handled (with some effort on your part, of course) within this course project, the following is a list of example systems and properties. This list should not be taken as a list of systems from which you should choose. In fact, you should try to choose something outside this list whenever possible. This list is just to give you an idea of the scale of a system that can be reasonably verified using existing tools in this course project. So please go through this list keeping this in mind.

  • TCP/IP protocol
  • Cache coherence protocols used in multi-processor systems.
  • Mutual exclusion protocols for sharing common resources.
  • Small modules of Linux kernel -- say file locking module or thread scheduling module, etc.
  • A collection of sorting programs -- say bubble sort and heap sort.
  • Small embedded systems software -- e.g. software for fuel injection in automobiles, or authentication software for smart cards.
  • Timing dependent systems -- e.g. traffic light controllers, chemical plant control software.
  • Device drivers for Linux/Windows
  • Protocols used in push-pull architectures for data dissemination e.g. stock data, news feeds on web browsers.
  • Bus protocols, like PCI bus, AMBA bus, TTA bus
  • Distributed database updation protocols. The above is only meant as a suggestive list. We would really like each group to come up with a problem from a domain that interests the group members. After choosing a system, you can then try to zoom down on a few properties that are interesting to check for the system. For example, for device drivers, it shouldn't be the case that the device gets locked indefinitely. Neither should it be the case that a particular invokation of the device driver messes up the result of the next invokation. Similarly for a bus protocol, you might want to check that no driver (master or slave) can cause another driver to starve indefinitely, or that a deadlock cannot happen.

    Once you have identified a system and a set of properties, send an email to the instructor and the TA, so that we can quickly determine whether it is too simplistic, too complex or of the right scale. Once this is done, you should identify a tool to be used for the verification. This should be done over email/personal meetings with the instructor and/or the TA.

    After identifying a system, properties and a tool, you must get down to modeling the behaviour of the system in the input language of the tool. You must also model the properties you want to verify in the input language of the tool. This will require you to learn a bit about the input language of the tool, but most tools have fairly understandable input languages and come with reasonably good tutorials and examples. Once the modeling of the system and specification of properties is done, you must run the tool to check if the property is satisfied. Typically, this will require a few iterations, where the modeling has to be modified/refined or the property stated in a certain way or some specific options of the tool have to be exercised. Finally, after each property has been checked and found to hold/not hold, you must write a report (not more than 5 pages) describing what you learnt from the entire exercise. You must also demo your verification process to us. The demo and the report will contribute towards your project score.

    Please send email to the instructor and the TA if you have any doubts/queries.