Time-Predictable and Composable Architectures for Dependable Embedded Systems

Organizers

Prof. Kees Goossens (Eindhoven university of technology)
Prof. Saddek Bensalem (Verimag, University Joseph Fourier)

Overview of the tutorial

Embedded systems must interact with their real-time environment in a timely and dependable fashion. Most embedded-systems architectures and design processes consider "non-functional" properties such as time, energy, and reliability as an afterthought, when functional correctness has (hopefully) been achieved. As a result, embedded systems are often fragile in their real-time behaviour, and take longer to design and test than planned. Several techniques have been proposed to make real-time embedded systems more robust, and to ease the process of designing embedded systems, including

Precision-timed and time-triggered architectures, to make time a first-class citizen of system design.
Deterministic architectures for repeatable timing behaviour.
Composability, which guarantees that the (non)-functional behaviour of components is unchanged on integration in a larger system.

The aim of this tutorial is to present the state of the art and major approaches to time-predictability and composability, such as BIP, TTA, PRET, PTIDES, Giotto, TipToe, and CompSOC.

Slides are now online below

Prof. Sifakis - Rigorous Component-based System Design in BIP
Prof. Obermaisser - Time-Triggered Architecture -- Concepts, Applications and Research Challenges
Prof. Goossens - Composable Timing and Energy in CompSOC
Prof. Lee - Repeatable Timing in Software and Networks
Prof. Kirsch - The Logical Execution Time Paradigm

The tutorial abstract that is in the proceedings:
"Time-predictable and composable architectures for dependable embedded systems"

Speakers

In alphabetical order:

Prof. Kees Goossens received his PhD from the University of Edinburgh in 1993, on the formal verification of hardware, in particular by using semi-automated proof systems in conjunction with formal semantics of hardware description languages. After several post-doctoral positions he joined Philips Research in the Netherlands in 1995. He led the team that defined te Aethereal network on chip for consumer electronics, where real-time performance and low cost are major constraints. His DATE'03 paper was selected as one of the 30 most influential papers of 10 years of the DATE conference. He was also part-time full professor at the Delft university of technology from 2007 to 2010, and is currently full professor at the Eindhoven university of technology, where his research focusses on composable (virtualised), predictable (real-time), low-power embedded systems.
Prof. Christoph Kirsch is full professor and holds a chair at the Department of Computer Sciences of the University of Salzburg, Austria. Since 2008 he is also a visiting scholar at the Department of Civil and Environmental Engineering of the University of California, Berkeley. He received his Dr.Ing. degree from Saarland University, Saarbruecken, Germany, in 1999 while at the Max Planck Institute for Computer Science. From 1999 to 2004 he worked as Postdoctoral Researcher at the Department of Electrical Engineering and Computer Sciences of the University of California, Berkeley. His research interests are in concurrent programming and systems, virtual execution environments, and embedded software. Dr. Kirsch co-invented the Giotto and HTL languages, and leads the JAviator UAV project for which he received an IBM faculty award in 2007.
Prof. Edward A. Lee is the Robert S. Pepper Distinguished Professor and former chair of the Electrical Engineering and Computer Sciences (EECS) department at U.C. Berkeley. His research interests center on design, modeling, and analysis of embedded, real-time computational systems. He is a director of Chess, the Berkeley Center for Hybrid and Embedded Software Systems, and is the director of the Berkeley Ptolemy project. He is co-author of six books and numerous papers. He has led the development of several influential open-source software packages, notably Ptolemy and its various spinoffs.
Prof. Obermaisser is full professor for Embedded Systems at the Department of Electrical Engineering and Computer Science of the University of Siegen in Germany. In February 2004, he has finished his doctoral studies in Computer Science at Vienna University of Technology. In July 2009, he received the habilitation certificate for Technical Computer Science. Roman Obermaisser is the author of numerous journal papers, books and conference publications.
Prof. Joseph Sifakis is a CNRS researcher at Verimag laboratory in Grenoble, France. He is recognized for his pioneering work on system design and verification. He contributed to the emergence of the area of model-checking, the most widely-used method for the verification of industrial applications. For his contribution to the theory and application of verification, he received the Turing Award in 2007. His research interests include component-based design, modeling, and analysis of real-time systems with focus on correct-by-construction techniques.

Registration

This tutorial is part of the embedded systems week. Please visit this website to register for this tutorial and the other events that take place during the ESWEEK.

Abstracts of the presentations

Prof. Sifakis - Rigorous Component-based System Design Using the BIP Framework

Rigorous system design requires the use of a single powerful component framework allowing the representation of the designed system at different levels of abstraction, from application software to its implementation. Such a framework allows to maintain overall coherency and correctness of the design flow by comparing different architectural solutions and their properties. We present a rigorous design flow using the BIP Behavior, Interaction, Priority) component framework as a unifying semantic model to derive correct implementations from application software, a model of the target architecture and a mapping. Correctness of implementations is ensured by application of source-to-source transformations in BIP which preserve essential design properties. The design flow is fully automated and supported by a toolset including a compiler, the D-Finder verification tool and model transformers. It is illustrated through two rivial case studies.

Prof. Lee - Repeatable Timing in Software and Networks

All widely used software abstractions lack temporal semantics. The notion of correct execution of a program written in every widely-used programming language today does not depend on the temporal behavior of the program. But temporal behavior matters in almost all systems. Even in systems with no particular real-time requirements, timing of programs is relevant to the value delivered by programs, and in the case of concurrent programs, also affects the functionality. In systems with real-time requirements, such as most cyber-physical systems, temporal behavior affects not just the value delivered by a system but also its correctness.

In this talk, we will argue that time can and must become part of the semantics of programs for a large class of applications. To illustrate that this is both practical and useful, we will describe two recent efforts at Berkeley in the design and implementation of timing-centric software systems. On the design side, we will describe PTIDES, a programming model for distributed real-time systems. PTIDES rests on a rigorous semantics of discrete-event systems and reflects the realities in distributed real-time, where measuring the passage of time is imperfect. PTIDES enables deterministic time-sensitive distributed actions. It relies on certain assumptions about networks that are not trivial (time synchronization with bounded error and bounded latency), but which have been shown in some contexts to be achievable and economical. PTIDES is also robust to subsystem failures, and, perhaps most interestingly, provides a semantic basis for detecting such failures at the earliest possible time. On the implementation side, we will describe PRET machines, which redefine the instruction-set architecture (ISA) of a microprocessor to include temporal semantics.

Prof. Obermaisser - Time-Triggered Architecture -- Concepts, Applications and Research Challenges

This presentation gives an overview of the concepts, applications and research challenges of the Time-Triggered Architecture (TTA). The TTA supports complexity management through the straightforward composition of systems out of components. As the foundation for robustness, the TTA supports fault isolation, the selective restart of components after transient faults, and active redundancy. Security is addressed at all levels of the architecture. Energy efficiency is enabled through integrated resource management that makes it possible to individually reduce the power-requirements of components. The TTA is a platform architecture that provides a minimal set of core services and a plurality of optional services that are predominantly implemented as self-contained system components. Choosing a suitable set of these system components that implement optional services, augmented by application specific components, can generate domain-specific instantiations (e.g., automotive, avionics).

Prof. Kirsch - The Logical Execution Time Paradigm

Since its introduction in 2000 in the time-triggered programming language Giotto, the Logical Execution Time (LET) paradigm has evolved from a highly controversial idea to a well-understood principle of real-time programming. This tutorial provides an easy-to-follow overview of LET programming languages and runtime systems as well as some LET-inspired models of computation. The presentation is intuitive, by example, citing the relevant literature including more formal treatment of the material for reference. This is joint work with Ana Sokolova.

Prof. Goossens - Composable Timing and Energy in CompSOC

This presentation will overview of the CompSOC platform that enables multiple applications to be implemented, verified, and executed independently. Any mix of best-effort, soft and firm real-time applications can be integrated, without any interference between them. Composability holds for functional behaviour, but also for timing, energy, and power. Every application has its own time budget on processor tiles, network on chip, on-chip memories, and SDRAM off-chip memory, enabling end-to-end performance guarantees for real-time applications. Energy and power budgets per application on each processor tile allow each application to have its own (real-time) power manager, without causing interference.