Resilient embedded systems

Mission

The resilient embedded systems research area explores the secure and dependable design and implementation of computing systems subject to stringent timing and resource constraints.

Real-time and embedded systems are virtually part of most modern technologies such as cars (e.g., engine control, anti-lock brakes, etc.), airplanes (e.g., fly-by-wire), or robotics (e.g., signal processing, actuator control). In such safety-critical domains, embedded real-time systems must be predictable, dependable and secure in the sense that correct outputs must always be produced at the right time, often under the presence of malicious actions. These requirements must be fulfiled on a tight resource budget, as embedded systems are commonly deployed in environments that impose severe space, weight, cost and power constraints.

Our research spans the entire range from the exploration of fundamental algorithmic issues to actual systems-building, and we particularly emphasize the intersection of both research approaches.

Publications

VatiCAN - Vetted, Authenticated CAN Bus

Deducing User Presence from Inter-Message Intervals in Home Automation Systems

Datenspeicherung in modernen Fahrzeugen – wem „gehören” die im Fahrzeug gespeicherten Daten?

A Tutorial on Human Activity Recognition Using Body-worn Inertial Sensors

Building timing predictable embedded systems

Blocking Optimality in Distributed Real-Time Locking Protocols

Basic Problems in Multi-View Modeling

Deductive control synthesis for alternating-time logics

Edit Distance for Timed Automata

Reverse engineering of cache replacement policies in Intel microprocessors and their evaluation

Extrapolation and Prediction of User Behaviour from Wireless Home Automation Communication

A Model-Based Certification Framework for the EnergyBus Standard

A Pipelined Multi-core MIPS Machine -- Hardware Implementation and Correctness Proof

Automatic Compositional Synthesis of Distributed Systems

Detecting Unrealizable Specifications of Distributed Systems

Fast DQBF refutation

JTACO: Test Execution for Faster Bounded Verification

Petri Games: Synthesis of Distributed Systems with Causal Memory

Security and Privacy Challenges in On-The-Fly Computing

A compositional modelling and analysis framework for stochastic hybrid systems

A Fully Preemptive Multiprocessor Semaphore Protocol for Latency-Sensitive Real-Time Applications

An Internet Inspired Approach to Power Grid Stability

An asymptotically optimal real-time locking protocol for clustered scheduling under suspension-aware analysis

Compositional Verification and Optimization of Interactive Markov Chains

Compositional Equivalence Checking for Models and Code of Control Systems

Efficient partitioning of sporadic real-time tasks with shared resources and spin locks

Improved analysis and evaluation of real-time semaphore protocols for P-FP scheduling

Multiprocessor Feasibility Analysis of Recurrent Task Systems with Specified Processor Affinities

Modelling, Reduction and Analysis of Markov Automata

Measurement-based modeling of the cache replacement policy

Precise timing analysis for direct-mapped caches

On Spin Locks in AUTOSAR: Blocking Analysis of FIFO, Unordered, and Priority-Ordered Spin Locks

Supervisor Synthesis for Controller Upgrades

Schedulability Analysis of the Linux Push and Pull Scheduler with Arbitrary Processor Affinities

The OMLP family of optimal multiprocessor real-time locking protocols

A Holistic View of Security and Privacy Issues in Smart Grids

FPGA-accelerated Key Search for Cold-Boot Attacks against AES

Privacy Enhanced Architecture for Smart Metering

Smart Grid and Method for Operating a Smart Grid

Dependability Results for Power Grids with Decentralized Stabilization Strategies

An Empirical Evaluation of the Influence of the Load-Store Unit on WCET Analysis

Modelling and Decentralised Runtime Control of Self-stabilising Power Micro Grids

Model Checking Algorithms for Markov Automata

Quantitative Models for a Not So Dumb Grid

State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems

Simulation and Statistical Model Checking for Modestly Nondeterministic Models