Skolan för
och kommunikation
KTH / CSC / Kurser / DD2452 / form09 / Labs

Formal Methods, form09

DD2452 Formal Methods: Labs

Laboratory Assignments

There will be two laboratory assignments:
  1. ESC/Java Lab. The first lab assignment is on using ESC/Java2 for program verification. 
  2. 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.

Copyright © Sidansvarig: Dilian Gurov <>
Uppdaterad 2009-01-12