Formal methods - Homework assignment (2017 Spring)

Content:

The homework assignment

To fulfill the requirements of the course, a homework assignment must be solved and submitted.

During the homework, a system specified by free text should be described with a formal model, on which you will have to check the given requirements with model checking. 

  • The system described in the assignment must be modeled with (timed) automata in the UPPAAL tool.
  • The given requirements must be formalized with temporal logic formulas and checked with the verification module of UPPAAL.

The goal is to gain experience in formal modeling and verification. The formal model may be created in several different (valid) ways, but we require the model to conform to the informal specification provided in the assignment.

The scenario of completing the homework assignment is the following.

  1. Create the formal model of the informally specified system in UPPAAL.
    • Briefly document the structure of the model, the considered alternatives (if any) and the nontrivial constructs that you used.
    • Explain and justify the modeling decisions you made (if any).
    • If necessary, refine the informal specification (to account for underspecified parts).
  2. Formalize the informal requirements provided in the homework assignments with the temporal expressions of UPPAAL.
    • Document the formalized requirements.
  3. Check on the model the satisfaction of the requirements with the verification module of UPPAAL using the formalized expressions.
    • Document the results of the verification.
    • If the verification of a requirement failed (i.e. it is not satisfied by the model), interpret the counterexample to find out what went wrong and fix the model if possible (unless asked otherwise by the assignment).

During the design of the formal model, it is recommended to proceed with step-by-step refinement, documenting each step.

The homework assignment is an independent work. Since only a limited number of tasks are assigned, there will be multiple students working on the same task. During modeling, you may discuss the assignment with the others, but we ask you to primarily work on your own. The documentation should be prepared individually, without any discussion with the others! This is how you demonstrate that - even if you received help before - you have understood and learned the basics of formal modeling. Therefore, copied or excessively resembling documentations will not be accepted!

Tools to do the homework assignment

The model checking task should be done with the UPPAAL tool developed by the Information Technology Department of the Uppsala University and the Computer Science Department of the Aalborg University. UPPAAL provides an integrated environment for the modeling and analysis of distributed systems with the help of timed automata networks. Checking the correctness of the behavior (the verification of the model) is supported with a restricted form of computation-tree logic (CTL). Models in UPPAAL can be built using an extended set of data types (bounded integers, arrays, etc.) and simple functions.

The user interface of UPPAAL is written in the Java language. This means that the Java runtime environment is necessary to run the tool (e.g. J2SE Java Runtime Environment).

The current version of UPPAAL can be downloaded after registration from the UPPAAL webpage. Educational usage is free of charge.

  • We have experienced problems with the registration and downloading when using Internet Explorer 9. In this case, a different browser will usually solve the problem.
  • If the installed official version has errors, trying the development version or occasionally running the tool from the IP domain of BME (to refresh the license file) may solve the problem.

The following resources can be of help with the usage of UPPAAL and its modeling language:

Furthermore, it is recommended to study the sample models provided with the tool and the Help menu.

Tasks and their assignment to students

Every student can look up their task and supervisor based on their Neptun code:

  • Assignment of tasks to students: Neptun code - Task ID pairing.
  • Those who requested us to accept their previously defended submissions (if we have accepted the request) do not have to submit a new task.

The task descriptions (i.e. the informal specification of the system to be modeled and the requirements) as well as the assigned supervisors can be seen below:

Task ID Task title Assigned supervisor
1 TCP Ákos Hajdu
2 Cache coherence Ákos Hajdu
3 Peer-to-peer overlay Dániel Élő

 

 

Consultation opportunity

On the 10th week of the semester (the week before the submission deadline) we offer an opportunity to ask questions about the tasks from the assigned supervisors.

Attending the consultation is not mandatory, but we kindly ask you to use this opportunity to contact your supervisor in case you have questions. If you cannot attend the consultation due to a collision with your timetable, please notify your supervisor in e-mail to find a suitable time. If you plan to arrive in the second hour of the consultation, notify your supervisor in advance in e-mail.

The time and place of consultation will be filled in the table below.

Task ID Task title Assigned supervisor Time and place
1 TCP Ákos Hajdu 18. April, 18:00-19:00 (IL405)
2 Cache coherence Ákos Hajdu 18. April, 18:00-19:00 (IL405)
3 Peer-to-peer overlay Dániel Élő 18. April, 18:30-19:30 (IL405)

Submission of the homework assignment

We require the following artifact to be submitted:

  • Detailed documentation of the solution (textual description with figures) in accordance with the scenario above.
    The documentation should contain the description of the model and its verification, the results and the explanation and justification of the design decisions. The document should be in PDF format. 
  • Source files of the UPPAL model and the queries.  

All these artifacts should be submitted in a single ZIP archive.

Please make sure to include the following data in the documentation:

  • Personal details (name, Neptun code),
  • Task title (not the ID only!).

The solutions must be submitted in email: molnarv _at_ mit.bme.hu.

Submission deadline: 29. 04. 2017. (Saturday), 23:59:00

After the submission deadline, we accept delayed submissions only (see below for details).

Defending the submission

After submitting the homework assignment, the solution has to be presented to the supervisor in person (defence). The purpose of the defence is to make sure the student completed the assignment on their own, using only permitted sources of help. During the defence, short questions will be asked about the modeling task and the submitted documentation. The rating of the submission will be finalized during the defence.

Due to the individual presentations, we expect students to apply for time slots in order to reduce the waiting time. The schedule of the defence and the application forms will be available in the table below.

  • We kindly ask you to apply for a single slot only.
  • In case of a delayed submission, the defence will also occur later in the repetition period, so in this case, students should apply there. Those who cannot attend the defence should also apply for the delayed defence.
  • Students must attend the defence in person. Failing to do so invalidates the submission! If attending the selected time slot has serious obstacles, contact your supervisor to schedule a new appointment!
Task ID Task title Assigned supervisor Application form (normal) Application form (delayed submissions)
1 TCP Ákos Hajdu https://doodle.com/poll/3sx942whcrsdkg73  
2 Cache coherence Ákos Hajdu https://doodle.com/poll/3sx942whcrsdkg73  
3 Peer-to-peer overlay Dániel Élő https://doodle.com/poll/kkha7mip7ge3qddg  

Delayed submission

After the submission deadline, we accept delayed submissions only. The delayed submission has a 20% penalty in score (one grade less). If you completely fail to submit a solution, you will fail the course!

Delayed submissions should also be sent in e-mail: molnarv _at_ mit.bme.hu.

Delayed submission deadline: 17. 05. 2017. (Wednesday), 23:59:00.

The artifacts to submit are the same as in case of normal submissions (documentation, models, results). The defence is still part of the homework, which will take place in the repetition period.

Time of defence for delayed submissions: The time and place of defence for delayed submissions can be found in the table above.
At the same time, normally submitted but potentially delayed defences may be held.

Results of the homework assignment 

The grading of the submissions will be finalized during the defence.

  • The results will be here after the defence.