02224 Modelling and Analysis of Real-Time Systems        Spring 2024
Baggage Sorting Project

Assignments

The course comprises two assignments (deadlines in parenthesis):

Mandatory Assignment 1 (Friday March 22, 2024, at 23.59)

 

Baggage Sorting Facility

A modelling and verification assignment using UPPAAL.

Mandatory Assignment 2 (Tuesday May 21, 2024, at 23.59):

 

Baggage Sorting Facility (contd.)

A continuation of part a comprising an elaboration and implementation of the system in Java.

See DTU Learn for the other Assignment 2 options.

Practical Details

Reports and files for each assignment must be uploaded to DTU Learn as described in the assignment.

The optional tasks should be done independently as extensions/elaborations of the basic common work. So there would typically be a common model for the common parts (1.-6.) and additional models/programs for the various optional tasks.

Detailed instructions and other information:

• The SingleSort.java program.

• Instructions for using the simulator for the LEGO construction.

• The RunSimulation.java simulation driver program. Use for inspiration if you are testing your own controller.
• Instructions for writing programs for the LeJOS environment.

Amendments and Errata

It is possible that certain parts of the assigment descriptions will have to be clarified or augmented. Such notes will appear in this section. So check this page if you encounter problems.

• April 9: The simulator has been updated to version 2.8 which fixes that the program had become outdated(!).
• April 9: Tips about stopping the belt for a multiple of Delta times have been added at the end.
• March 14: See update on scalar types below

Tips

Below are some tips for issues that are commonly encountered in UPPAAL modelling.

• If your UPPAAL model behavies totally weird, check that you did not incidentally create two locations on top of each other (try to move a location and see if there is another one behind).

  [Many professor and student hours have been wasted due to this ``feature".]

• In UPPAAL, in order to take a transition as soon as its guard B becomes true, you should not put !B as an invariant of the source location. This will just prevent B from ever becoming true and will result in an error message like Undefined next state ....

  Instead, use the standard technique of declaring an urgent broadcast channel, say go, and add the synchronization go! to the transition.

• Use of committed states for sequences of local actions in the control part will reduce the verification state space.
• Use of type declarations simplifies instantiation of automaton templates with a single parameter and also verification of properties of these instances.

  Consider a template T with a single parameter int id. Creating two instances of this template could be done as follows in System declarations:
  

  T0 = T(0);
  T1 = T(1);
  system T0, T1;

  Creating many instances could be tedious to make, instead type definitions can be used to ease this task. The above mentioned example could be instantiated by defining a type, say t_id, for the parameter id instead of int in Declarations as follows:
  

  const int N = 2;
  typedef int[0,N-1] t_id;

  In order to change the number of instances of the template to be created, only the value of the constant N needs to be modified. Instantiation is done in System declarations simply by adding the template to the system as follows:
  system T;

  Verification of predicates in all or some of these templates can easily be done with the operators forall and exists, e.g. checking reachability for all instances of T reaching the local state B:
  

  E<>forall(i:t_id)T(i).B

  Alas, these quantifiers cannot be used with leads-to properties for which explicit enumeration must be made.

  The example specified here can be seen in the file: instantiation.xml

• If the values of a type are only used for enumeration of instances and not for a particular ordering, the index range may instead be declared as a scalar type:

  const int N = 2;
  typedef scalar[N] t_id;

  In that case, the verifier can use symmetry reduction to eliminate permutations of instances reducing the verification considerably.

  This example can be found in the file: scalar_instantiation.xml

  Update:
  The benefits of using scalar types are only applicable for invariant queuries (A[]) or possibility queries (E<>).

  For leads-to properties (-->) scalar types have no effect and it may not even be possible to state relevant properties as specific template-instances (such as T(0)) cannot not be referred to.

  Thus: Use scalar types for verification of safety properties (invariants), but replace them with integer range types when verifying liveness properties.

• If you use a fixed stop position, you may have troubles stopping the motor at the exact time before the bag moves on. A principal solution for this problem can be found here:

      fixedpos.xml.

• If you allow only a single stop point on the feed belt, any attempt to stop elsewhere should be detected and recorded as an error.

  You should then verify that such errors will not occur when your control strategy is applied.

• Likewise, if you use fixed stopping times, your model should detect if this is indeed the case. You may look at the basic example:
  stopping.xml.

  A more elaborate example of fixed period stopping is:
  multistop.xml which demonstrates how to use stop periods which are multiples of some Delta time