Verification of Real-Time Systems

Organizers

News

Note that the date of the exam has changed.

Time and Place

The lecture takes place on Thursdays from 2-4pm in lecture hall 1 in building E1 3. The first class is on April 23. There will be no class on May 14 and June 4, since these are official holidays.

There tutorial takes place weekly on Mondays from 12-2pm in seminar room U12 in building E1 1. The first tutorial is on May 4.

Introduction

Real-time systems play a crucial role in many applications, such as avionic control systems, automotive electronics, telecommunications, industrial automation, and robotics. Such safety-critical applications need to be implemented correctly to prevent serious damage to the environment or even the loss of human lives.

In this course, we will study methods to verify the timing behavior of such systems. In particular, this includes fundamentals of worst-case execution time analysis and real-time scheduling theory. In addition to analysis methods, we will also discuss the design of timing-predictable hardware platforms that ease analysis.

Prerequisites

While there are no specific course prerequisites for this advanced course, a solid background in discrete mathematics is highly recommended, as provided by undergraduate math courses in our bachelor's program. In addition, some C++ programming experience would be valuable for the practical projects.

Schedule

Date Title Recommended Reading
April 23, 2013 Introduction to Real-Time Systems -
April 23+30, 2013 Introduction to WCET Analysis (Revision 1) -
April 30, 2015 Foundations of Abstract Interpretation I Abstract Interpretation in a Nutshell
May 7, 2015 Foundations of Abstract Interpretation II -
May 14, 2015 public holiday, no class -
May 21, 2015 Numerical Abstractions
Loop Bound Analysis		 -
May 28, 2015 Static Cache Analysis
Relational Cache Analysis		 Caches in WCET Analysis (Chapter 4)
Relational Cache Analysis
June 4, 2015 public holiday, no class -
June 11, 2015 Beyond Least-Recently-Used
 Timing Predictability of Cache Replacement Policies
Relative Competitive Analysis of Cache Replacement Policies
June 18, 2015 FIFO Cache Analysis I
FIFO Cache Analysis II
Cache Persistence Analysis for LRU
 Abstract Interpretation of FIFO Replacement
Precise and Efficient FIFO-Replacement Analysis Based on Static Phase Detection
June 25, 2015 Persistence Analysis for FIFO, MRU, PLRU
Microarchitectural Analysis
Path Analysis		 -
July 2, 2015 Predictability and Predictable Microarchitectures
Precision-Timed ARM 		-
July 9, 2015 Task Models and Scheduling RL Graham: Bounds on multiprocessing timing anomalies
Giorgio Buttazzo: Hard real-time computing systems : predictable scheduling algorithms and applications, Chapter 2+3
July 16, 2015 Schedulability Analysis of Periodic Task Sets under Fixed-Priority Scheduling (Revision 1) Giorgio Buttazzo: Hard real-time computing systems : predictable scheduling algorithms and applications, Chapter 4
July 23, 2015 Schedulability Analysis of Periodic Task Sets under Dynamic-Priority Scheduling

Resource Sharing in Real-Time Scheduling

 Giorgio Buttazzo: Hard real-time computing systems : predictable scheduling algorithms and applications, Chapters 7
July 30, 2015 Cache-Related Preemption Delay in Response-Time Analysis

 -

Assignments

Deadline Assignment Material
May 7, 2015 Assignment 01 -
May 14, 2015 Assignment 02 -
May 21, 2015 Assignment 03 -
May 28, 2015 Assignment 04 -
June 4, 2015 Assignment 05 -
June 11, 2015 Assignment 06 -
June 18, 2015 Assignment 07 -
June 25, 2015 Assignment 08 -
July 2, 2015 Assignment 09 -
July 9, 2015 Assignment 10 -
July 16, 2015 Assignment 11 -
July 23, 2015 Assignment 12 -

Exam

The "end of term" exam will take place after the end of the lecture period on August 5 from 10:00 to 12:00 in lecture hall 1 in building E1 3. A reexam will be offered on demand at the end of the semester.

To be admitted to the exam, at least 50% of the points in the assignments are required.

Recommended Literature

  1. Giorgio Buttazzo: Hard real-time computing systems : predictable scheduling algorithms and applications
  2. Edward Ashford Lee, Sanjit Arunkumar Seshia: Introduction to embedded systems : a cyber-physical systems approach
  3. Peter Marwedel: Embedded system design: embedded systems foundations of cyber-physical systems