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 3. However, if you want to work on the assignment in a group of 2 or 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 (March 28 at the latest), I want you to send me a report explaining your model and analysis results. 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. Evaluate the quality of the model using the criteria described in section 1.10 of the paper A First Introduction to Uppaal.
  2. 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.
  3. 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?
  4. 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.
• Leader Election.
  
• Leader election in OSPF
  
• Sudoku Solving. Sudoku's can naturally be viewed as transition systems: states are Sudoku grids and there is a transition if one grid can be obtained from another grid by filling in values one or more empty squares. Solving a Sudoku then corresponds to a reachability problem: does there exist a path leading to a state in which there is no empty square. The topic of this assignment is to explore the use of Uppaal for solving Sudoku's:
  1. Construct a Uppaal model for solving Sudoku's.
  2. If you just build a naive model in which in each step Uppaal guesses a number and fills a square, you will hit the state space explosion problem. So you need to be smart. Show that your optimized solution can solve all (or at least many) of the hardest Sudoku's listed on Wikipedia and on http://magictour.free.fr/sudoku.htm. (You may want to write a small script that turns a specification of a Sudoku puzzle into a Uppaal model for solving it.)
  3. How does your Uppaal Sudoku puzzle compare to other solvers? Are there examples where Uppaal performs particularly bad?
  4. Are there algorithmic ideas for solving Sudoku's that cannot be incorporated in your Uppaal model? How about the Dancing links algorithm of Knuth, for instance? Would it make sense to extend Uppaal at these points? (That is, would such techniques also be useful for other verification problems?)
  5. Many algorithms for Sudoku's have been proposed, but as far as I know thus far no constant time complexity bound was established ("If there is a solution then Uppaal will find it within 10 seconds"). If you manage to prove such a result then this may be worth publishing. (NB On the download page on Uppaal website your find a small utility, called Memtime, for measuring time and memory consumption.)
  Warning: This problem has no relation with embedded systems whatsoever!! I just added it because it looks like a fun problem and may give some insight on the expressive power of Uppaal modeling and search.
  
• Serial ATA. Last month, Intel announced a serious flaw in the Sandy Bridge chipset. Intel estimates the total costs of this bug will be 700 million dollar, making it about twice as expensive as the famous Pentium bug. Due to problems with one transistor, the functionality of some Serial ATA ports may degrade over time. Even though the source of the problem was at the electrical rather than at the protocol level, see http://www.anandtech.com/show/4143/the-source-of-intels-cougar-point-sata-bug, it would be very interesting to take a closer look at the Serial ATA protocol How does this protocol work? Can we make a Uppaal model of parts of Serial ATA standard, in particular the 8b/10b encoding and the clock synchronization aspects, and prove correctness (or find another 700 million dollar bug)?
  Warning: This is the real thing! This assignment is difficult and challenging. The Serial ATA standard is 310 pages, including lots of electrical engineering stuf! A major challenge here is to extract a fragment of the standard that is amenable to formal specification/analysis using model checking. The instructor will help you though to get on the right track.