Formal Methods for Software Development TDA294/DIT271, LP1, HT2019

Lab Assignments

General Remarks

We will have two labs during the course. Each submission of a lab is either rejected (meaning you must improve it) or accepted (meaning you have passed the lab). If the first submission is rejected you have ca. one week to resubmit a corrected version. You must do the labs in pairs.

Groups must be formed, and registered in the Fire system (see below) until and including Friday, September 13 2019.

Needless to say, each lab group must produce their own solution. If we catch you copying the solution of someone else, then this will have serious consequences. Among them is that you will fail the course.

If you have questions regarding the labs, you are encouraged to post them to the course's Google group.

Submission of labs is handled through the Fire reporting system, see below.



The Lab Assignments

The links will be activated before the first lecture on the topic of the lab takes place.

  • Lab 1: Promela/SPIN:
    Specification of Promela models, writing safety properties in Temporal Logic, using SPIN for verification.
    Deadline: Friday, October 4 2019 23:59
    Final Deadline: Monday, October 14 2019 23:59

  • Lab 2: JML/KeY:
    Specifying contracts and invariants for a Java program in JML, verification of correctness with KeY.
    Deadline: Monday, October 28 2019 23:59
    Final Deadline: Thursday, November 7 2019 23:59



  • Reporting

    The assignments must be handed in using the Fire report system

    Before you submit: Create an account and join a lab group

    The first step is to register yourself/your lab group in the submission system. This has to be performed only once for all labs and works as follows:

    1. Go to the system site, click on "Register here" and fill in the requested information. Students without "personnummer" can use their Chalmers- or GU-number.
    2. Log on using the account you just created. One of the group members should create a new group and the other one should join that group.
    3. The selected group is used as your default group for both labs.
    4. If you want to hand one lab as a member of a different group, you can click on "Leave group" and select another one.

    Submitting a lab assignment

    1. Log on to the submission system (for a group of two persons it does not matter which one is submitting the solution, as long as both persons have joined the group).
    2. Upload the files that make up your solution for the lab. Make sure that your solution is in accordance with the description of the lab regarding file formats, output of programs etc.
    3. Once all files are uploaded, you can submit your solution.
    4. As soon as your submission has been reviewed (that means either accepted or rejected) you will receive a mail.
    5. You can possibly download comments to your solution: Therefore you have to log on to the submission system again and display the files called comment.
    6. In the case of a rejected solution you will have to upload a corrected version and submit again.



    W. Ahrendt, Jul 18, 2019