COEN 7311: Winter 2012 Project Description

NB! As a team, you a choice between

1) Survey Paper ( Research oriented),

OR

2) Project (Applied)

The goal of the project is to use a description language (Promela - Protocol Meta Language) to model and describe the Trivial File Transfer Protocol - TFTP (an Internet Standard) with Option Extension, and experiment with simulation and verification using SPIN.

You can run "tfpt" on your local Unix/Linux station.   

We will discuss the Trivial File Transfer Protocol in class during the lectures

The basic references for TFTP are: RFC 1350 and RFC 783

TFTP Option Extension allows for negotiations prior to the transfer. You have to model TFTP with 3 extensions: Timeout interval, Transfer size, and Window size options (size 1, 3, or 7). For Option Extension, you have the following RFCs:
RFC 2347
RFC 2348
RFC 2349

TFTP runs on top of UDP (User Datagram Protocol).

You should read carefully the informal descriptions before starting your design/modeling. An important part of the project is to understand the informal description and develop a formal one in Promela.

Your MODEL has to be SIMULATED and VALIDATED using SPIN. You will have to VERIFY (using SPIN) the following specific properties.

If you wish to study another protocol, make your suggestions to the instructor. However, keep in mind that it should be at least of the size of the Trivial File Transfer Protocol. You may choose another protocol from the internet standards, here is a link to the RFCs. BEFORE YOU START WORKING ON ANY PROTOCOL, YOU SHOULD SEEK FOR AN APPROVAL FROM THE INSTRUCTOR.

A REPORT (between 20 and 30 pages) explaining your design, summarizing your experience in design, validation and use of SPIN should be submitted by March 30^th.

Date for Demos: Week of April 1st

You can work in teams of two students. In this case a report of one or two pages explaining the contributions of every member should be submitted in addition to the report mentioned previously.