Projects
There will be three smaller projects in Coloured Petri Nets 1 and a larger project in Coloured Petri Nets 2.
Coloured Petri Nets 1
- Project 1: CPN Modelling
- Project 2: CPN State Space Analysis
- Project 3: CPN Performance Analysis
Coloured Petri Nets 2
The fourth quarter is devoted to project work on construction and validation of a larger CPN model chosen by the students. The teacher will be available on-demand for discussion of the project work. In addition to this, we will all meet two times (where participation is mandatory). The detailed plan will be announced later.
The project report should be approximately 20 pages. In addition to this it is allowed to add a number of appendixes which show the full model, state space reports, etc. However, it should be possible to read and understand the 20 pages without consulting the appendices.
Project Proposals
The projects are to be conducted in groups of at most 2-3 persons and each group is free to define their own project. The project can be done in a number of application domains, and the groups are free to define their own project. Below is a list of proposals for systems that can be used as a basis for modelling and validation. Other suggestions from the course participants are also welcome.
Project 1: Mutual Exclusion Algorithms
Several mutual exclusion algorithms (such as Peterson's algorithm) have been proposed in the literature. The goal of this project is to model and verify 1-2 mutual exclusion algorithms. Several algorithms are described in, e.g., :
- M. Raynal: Mutual exclusion algorithms which is available in the IT library.
Project 2: NASA PathFinder
This project is concerned with building a CPN model of a selected part of the NASA PathFinder system and investigating the issues that led to the failure of the system. Inspiration for the project is available via:
- G. Holzmann: SPIN model checking: An Introduction. International Journal on Software Tools for Technology Transfer, 2000. Available via the IT library. This paper describes in detail the aspect of the system to focus on.
- Problem description. This web pages gives a lot of technical detail about the system. Not all of these are required to construct a model of the system.
Project 3: The Dynamic Host Configuration Protocol
This project considers the DHCP protocol described in RFC 2131. The aim of this project is to construct a CPN model of the DHCP protocol, formulate desired properties, and verify these using simulation and state space analysis.
Project 4: Gas Station
Consider a modern gas station with a number of customers, six different pumps and one operator. Construct a CPN model that captures the workflow of customers arriving at the gas station for buying gasoline, including selecting the gasoline, pumping the desired amount of gasoline, and paying. Payment could be by credit card or cash, and there is also the option of prepayment.
The constructed CPN model could either server as a basis for analysis the performance of the system using simulation, or verifying desired properties of the system using state space analysis
Project 5: Distributed File System
This project is concerned with modelling and validation of Network File System and/or Andrew File System described in Chap 8 of:
- G. Colouris, J. Dollimore, and T.Kindberg: Distributed Systems - Concepts and Design. Addison-Wesley, 2001. The book is available from the IT-library.
A possible focus could be on caching strategies and consistency.
Project 6: Replicated Architecture
This project is concerned with modelling and validation of architectures for active and/or passive replication described in Chap 14 of:
- G. Colouris, J. Dollimore, and T.Kindberg: Distributed Systems - Concepts and Design. Addison-Wesley, 2001. The book is available from the IT-library.
A possible focus could be on the correctness criteria.