Formal Methods, form09
DD2452 Formal Methods: Labs
Laboratory Assignments
There will be two laboratory assignments:
- ESC/Java
Lab. The first lab assignment is on using ESC/Java2 for
program verification.
- SPIN
Lab. The second lab assignment is on using SPIN for
verifying an
Internet standards track protocol, the Mobile IP protocol. Here is the Basic Mobile IP Promela
Model needed for the lab.
Labs can be done
in teams of two, or they can
be
done individually.
Collaboration between teams is fine at the level of exchange of ideas,
but each team must do its own work and is responsible for the
correctness and originality of their results.
For each lab, each
team must hand in a
report
explaining their solution, code, analysis
results
and conclusions. The report must be properly typed and written in
understandable
English or Swedish by you. All text not written by you must be properly
quoted.
The
report is handed to the course leader at the same time as the lab is
demonstrated,
at the scheduled slots.
Lab
reports/presentations
are pass/fail. They must be
produced at the
scheduled time, with acceptable quality.
