Formal methods - Homework assignment (2020 Spring)

Contents

The homework assignment

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

During the homework, a system specified informally (by free text) should be modelled using a formal model, on which you have to verify the given requirements using 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 description provided in the assignment.

The steps for completing the homework assignment are the following.

  1. Create the formal model of the informally described 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 description (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) then interpret the counterexample to find out what went wrong and fix the model if possible (unless asked otherwise by the assignment).

The homework assignment requires 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 solve the homework

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. Academic 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 reports errors, then trying the development version of the tool 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

The homework assignments can be found as follows:

  • Assignment of tasks to students: See here later.
  • Those who requested us to accept their successful homework from the previous semester (and we have accepted the request) do not have to submit a new homework.

Consultation opportunity

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

Attending the consultation is not mandatory, but we kindly ask you to use only this opportunity to contact your supervisor in case you have questions. If you cannot attend the consultation due to a conflict in your timetable, then please notify your supervisor in e-mail to find a suitable time.

The time and place of consultation are found in the table below.

Assigned supervisor Time and place of consultation
   

Submission of the homework

We require the following artifacts to be submitted:

  • Detailed documentation of the solution (textual description with figures) in accordance with the steps above.
    The documentation should contain the description of the model, the related explanation of the modelling decisions, and the verification results. The document should be in PDF format. 
  • Source files of the UPPAL model and the queries (formalized requirements).  

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),
  • Title of your homework assignment.

The solutions must be submitted electronically. Detials how to submit your homework will be given here.

Submission deadline: 9 May, 2020 (Saturday), 23:59:00.

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

Presenting the solution

After submitting the homework, the supervisor may ask you to present your solution in person. The purpose of this presentation is to make sure that you completed the assignment on your own, using only permitted sources of help. During the presentation, short questions will be asked about the modeling task and the submitted documentation. The grade of the homework will be finalized after this presenation.

The schedule of the required presentatios will be published here later.

Late submission

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

Late submissions should be submitted in the same way as in case of normal submissions (see above).

Deadline for late submission: 27 May, 2020 (Wednesday), 23:59:00.

The artifacts to submit are the same as in case of normal submission (documentation, models, results). After submitting the homework, the supervisor may ask you to present your solution (in person).

Results of the homework

The grading of the submissions will be published here later.