The report
The report should include the following:
-
The complete Promela code.
-
The modelling decisions you made, together with motivations if possible.
You could for example do this in the form of comments in the Promela code.
Per property to be checked:
-
An explanation of how you checked it: standard Spin check or LTL
formula; give an explanation of the formula; describe the meaning of any
variables introduced for checking; etc.
-
Your experiences while checking: was it found to be valid or did you have
to introduce extra assumptions; if so, which assumptions and
how did you encode them; state space considerations; etc.
-
The results of verifying the property for a number of configurations
of the system.
-
Explore what are the limits when you constrain Spin to the memory
constraints of your machine and explain the reduction techniques you appied.
Be precise about what you check and what the results are - include at least
the length of the state vector, the number of reached states, and the actual
memory used for states and the total memory usage.
A section with conclusions about verification of the
protocol. Make an attempt to view the results from a general point. Try
to give some ad-hoc reasoning that shows that the obtained results will
also hold for larger configurations, or for different modelling decisions.
It is not necessary to provide an introduction explaining the system.
Submission and deadline
The Promela code and related LTL files should be submitted by e-mail.
Please write down in each of the sources your name.
The rest of the report can also be sent by e-mail in Post
Script format. The alternative is to deliver a paper version to
me personally or leave it in my mail box (in front of the secretary's room
HG 7.45 ). Both the report and the model have to
be sent before March 7 2000. Please consider
this deadline as firm.
Evaluation
This final assigment will be evaluated based on the report and a discussion
of it during the oral examination. The report should satisfy the above
requirements in order to be sufficient. During the examination, you will
have to be able to explain what you have done and why.