First Assignment for AES Course: Modelling and Analysis with Uppaal

The goal of this assignment is to model and analyze a somewhat larger example using (a variation of) the timed automata model checker Uppaal. I prefer that you work on this assignment in groups of 2 or 3. However, if you want to work on the assignment on your own this is also allowed. According to the course planning, you are supposed to spend around 35 hours on this assignment. In the end (April 5 at the latest), I want you to send me a report explaining your model and analysis results. Evaluate the quality of your model using the criteria described in section 1.10 of the paper A First Introduction to Uppaal. Also send me the Uppaal models that you constructed. You may choose one of the following four problems:

• Battery Scheduling. In a system where multiple batteries can be connected, battery scheduling can be used to spread the workload over the individual batteries. In chapter 5 of his PhD thesis (based on an earlier conference publication), Marijn Jongerden uses the model checking tool Uppaal Cora to find schedules that lead to the longest system lifetime. Marijn kindly made his Uppaal model and slides available to us. The AES assignment is to study this model and to try to improve the results of Marijn. More specifically, consider the following questions:
  1. Marijn uses a modeling trick in Uppaal Cora to compute the longest system lifetime. However, it should also be possible to compute the longest system lifetime using regular Uppaal, using the binary search approach described at the end of section 1.8 of A First Introduction to Uppaal. Repeat Marijn's analysis using Uppaal and compare memory and CPU usage of the two approaches.
  2. The timed automaton model of Marijn is a discretization of the continuous KiBaM model. However, in the construction of the Uppaal model all kinds of simplifying assumptions are made. As a result, the relationship between the Uppaal model and the KiBaM model are not entirely clear. It would have been better to make the Uppaal model nondeterministic with timing intervals that overapproximate the timing of the KiBaM model. According to Marijn such models become to complex to analyze using Uppaal Cora. Can you make a model that is a more accurate reflection of KiBaM than Marijn's model and that can be analyzed using Uppaal? Can you give an estimate of the errors introduced by the simplifying assumptions of Marijn?
  3. Fix a scheduling policy, for instance best-of-two, sequential scheduling or round-robin, but make the arrival times of new tasks fully nondeterministic: we don't know when tasks arrive. Compute the worst case performance, that is, the shortest battery lifetime. Compare the worst case performance for different scheduling policies.
• The Welch-Lynch Fault-Tolerant Clock Synchronization Algorithm. The fault-tolerant algorithm for clock synchronization of Jennifer Lundelius-Welch and Nancy Lynch is a celebrated result in distributed computing. The algorithm is widely used, for instance as a basic synchronization mechanism in the timed triggered architecture of Kopetz, which is used in the automotive sector (FlexRay). The AES assignment is to make a Uppaal model of (a simplified version of) this protocol, and verify the correctness for some instances. A Uppaal model for the algorithm was constructed already in 2004 by Aceto, Behrmann, Groote and Larsen. However, this model was defined using an earlier version of Uppaal in which the syntax was much more restricted and the verification engine was less powerful. The importance of the algorithm makes that it deserves a new attack. Christian Mueller from Saarland University wrote some interesting notes on the verification of the algorithm (see also his slides). Of course, the more general your model is, the better. But in order to be able to verify some instances you will have to make some simplifying assumptions. In his manual proof, Mueller assumes that broadcasting a message, computing the adjustment, storing arrival time are instantaneous operations. A simplifying assumption made in time-triggered architectures is that only a single fault has to be tolerated. You may consider to construct two models: one general model that accurately describes the general algorithm, and a simplified model that may be verified.
• The PS/2 Keyboard and Mouse Protocol. The PS/2 Keyboard and Mouse Protocol describes the communication between a computer and a mouse or keyboard. PS/2 is considered a legacy port in modern computers (USB ports are preferred) but nevertheless they are still widely used. The AES assignment is to model and analyze this protocol using Uppaal, with emphasis on the system timing behavior as specified here. A number of timing parameters are specified (T1-T9) and for each timing parameter a minimal and maximal value is given. Does the protocol work correctly for all assignments within these intervals? Which constraints on T1-T9 are required for correctness?
• Synthesis of an Embedded Sensor Controller using Uppaal Tiga. Uppaal Tiga is an extension of UPPAAL that implements an on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. Uppaal Tiga has been used successfully to synthesize some controllers for embedded systems, see for instance the work of Cassez et al. In a recent paper Analyzing an Embedded Sensor with Timed Automata in Uppaal, Timothy Bourke and Arcot Sowmya, use Uppaal to model a very simple infrared sensor + the corresponding controller, and verify the correctness of the combined system. The AES assignment is to investigate whether it is possible to actually synthezise a controller for this sensor using Uppaal Tiga, taking the model of Bourke and Sowmya as a basis.