Lab assignment for Ph.D. students

  • Due No due date
  • Points 1
  • Submitting a website url or a file upload

Graded lab assignment for course FDD3463

Notice

Master's students can ignore this assignment; it is only relevant for students taking the Ph.D.-level course FDD3463.

Assignment

Instead of doing the other graded lab assignments, develop a formal model and a software-level model of an algorithm, architecture, or protocol that they are working on as part of their research. The high-level model will be developed in Event-B, NuSMV, or a similar tool that is suitable for formal verification; the low-level model (which may include only a part of the high-level model) will be written in a programming language like Java and verified with a tool like JPF or PAT.

Deliverables

  1. A high-level model for a modeling tool like Event-B, NuSMV, Spin, or similar. The tool must be openly accessible for KTH users (either as open-source software or by KTH having a license for it).
  2. A detailed model of the high-level model or a part of it, written in a programming language for which analysis tools like JPF or PAT, or symbolic execution tools like Klee exist.

You can link to a git repository containing your solution or upload a file. To post more than one link or file, use an attachment or write the second URL as a comment.

Grading

For the Ph.D. course, the grading is pass/fail.

0