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

Each student is assigned an individual homework.

  • The code of the homework is available on the hf.mit.bme.hu portal of the department. You can login with the BME Central Login system (preferred).
    This portal shall be used for the submission of your solution as well.
  • 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.

The set of potential homework assignments can be found in the table below. Please download your homework according to the code (HA01 ... HA07) that you find on the portal mentioned above.

Code Description of the homework
HA01 HA01 Coffee Machine
HA02 HA02 Traffic Lights
HA03 HA03 Peterson
HA04 HA04 Szymanski
HA05 HA05 DekkerN
HA06 HA06 Dijkstra
HA07 HA07 Eisenberg-McGuire

Consultation opportunity

On the 10th and 11th 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.

The date of online consultation is given in the table below. Details will be provided in Neptun message.

Assigned supervisor Date of consultation
Bence Graics April 28 (Tuesday), 2020, 16:00-17:00, MS Teams

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 UPPAAL 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 on the hf.mit.bme.hu portal of the department.

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 (online). 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. Further details will be provided for the concerned students in Neptun message.

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 electronically on the hf.mit.bme.hu portal of the department.

Deadline for late submission: 27 May, 2020 (Wednesday), 23:59:00 The 10th day of the examination period.

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 (online, in person).

After the evaluation of your homework assigment, we do not accept the repeated submission of the same task. In case you would like to improve your grade, we ask you to contact the course coordinator in email and we assign you a completely new task. The deadline for the submission of this new task is the same as given above (the 10th day of the examination period).

Results of the homework

The results (grading and evaluation) of the submissions are available on the hf.mit.bme.hu portal.