Analysis of Embedded Systems (I00154), Spring 2010

• 0. Instructor: Frits Vaandrager (HG02.622, phone: 365 22 16)

• 1. When and where:

  what	day	time	where
  lectures	Monday	10.45-12.30	HG01.029
  problem sessions	Wednesday	10.45-12.30	HG01.057

  First lecture on Monday February 8!!. Note: Since the expected number of participants for this course is small, it might be possible to change the schedule if this is convenient for the participants.

• 2. Information on the planning of the course, assignments and solutions is available via a special webpage. Announcements will be sent via email. Blackboard will not be used for this course, except for email.

• 3. Course material: The course material consists of hand-outs, sheets, and recent papers from the literature. These will be made available electronically via the course page or distributed during the course. Most of the theory discussed in the course is presented in the textbook Principles of model checking / Christel Baier; Joost-Pieter Katoen. - Cambridge, Mass.: MIT Press, 2008. ISBN 978-0-262-02649-9. This book is recommended but not mandatory.

• 4. Motivation/Overview: As our daily lives depend increasingly on digital systems, the reliability of these systems becomes a concern of overwhelming importance, and as the complexity of the systems grows, their reliability can no longer be sufficiently controlled by traditional approaches of testing and simulation. It becomes essential to build mathematical models of these systems, and to use (algorithmic) verification methods to analyse these models. During recent years there has been enormous progress in the areas of hardware and software verification. In this course, an overview will be presented of mathematical techniques for the specification and analysis of embedded systems. The application of these techniques will be illustrated on industrial sized examples taken from the areas of embedded real-time systems, distributed algorithms and protocols. Participants learn how to make models and how to analyze them using state-of-the-art techniques and tools.

• 5. Objectives:
  Objectives: After successful completion of the course, participants are able to:
  • recognize situations in which the applications of model checking techniques for specification and analysis may be useful,
  • explain the modelling frameworks and basic theory of finite state, real-time, and probabilistic automata,
  • model (critical parts of) embedded systems as networks of automata,
  • formalize desired properties of these systems in terms of automata or temporal logic, and
  • use state-of-the-art tools for analysis of realistic embedded system problems.

• 6. Topics:
  Theory: (symbolic) model checking, temporal logic, timed automata: difference bounded matrices, binary decision diagrams, bounded model checking, probabilistic automata, discrete-time Markov chains, Markov decision processes.
  Tools: Uppaal, SAL, PRISM
  Applications: Various controller synthesis and resource allocation problems from the embedded systems area, real-time operating systems, distributed algorithms and protocols: leader election for networks with ring, tree or general topology, mutual exclusion algorithms, communication protocols for physical and datalink layer.

• 7. Time investment: Participants are supposed to spend approximately 168 hours (=6ec) on this course: during 16 weeks they will need about 4 hours per week to attend+prepare classes (2 hours lectures, 1 hours problem session, 1 hour reading or working on exercises at home). In addition they will need about 35 hours for each of the three larger homework assignments (to be made in small groups of 2 or 3 participants) based on which their participation in the course will be evaluated. Participants are expected to be present during the lectures and the problem sessions.

• 8. Prerequisites: Familiarity with propositional and predicate logic, automata theory, basic complexity theory, and basic (graph) algorithms is assumed. For instance, you should know what a tautology is, how to formally prove a formula in predicate logic, how to determinize a finite automaton, what is the time complexity of sorting, and how to find the strongly connected components of a graph. The mathematics and theory courses from our bachelor curriculum will certainly provide enough background (frequently, I will refer to topics that have been previously addressed during the bachelor courses courses such as Discrete Wiskunde, Talen, Beweren en Bewijzen, Inleiding in de Complexiteitstheorie, Logica). If you are not familiar with the concepts, please see the instructor.

• 9. Grading: Grades will be awarded on the basis of three larger homework assignments, which participants may do on their own of in groups of at most three So instead of a final exam this course has "integrated examination". The final score is obtained as the average of the scores for the three assignments. If the final score is 5 or below, participants will be offered the opportunity to make a 4th homework assignment. The final score will then be the average of the 3 highest scores (so the lowest score may be dropped).

• 10. Combinations with other courses: This course is part of the embedded systems theme.
  

• 11. Course evaluations (in Dutch)