Centre Universitaire d'Informatique

Compositionality and Heterogenity: Formal Analysis of Constraint Systems

With Dr. Kai Lampka, ETHZ

Abstract:

When analyzing and designing embedded systems with hard real-time constraints contemporary methods abstract from individual events and their processing. In an abstract setting, one rather considers infinite streams of input stimuli provided by the environment to some task running on a computing device. Upon completion the task may emit (timed) events to the environment, which again may trigger computations in some down-streamed devices. When processing an event, a task can not process any other incoming event of the same type. Conflicting resource accesses of tasks is resolved by some scheduling policy, e.g. earliest-deadline-first (EDF), priority-based, etc.. Event streams, and tasks sharing computing devices and communicating via (non-blocking) FIFO-buffers of infinite capacities are the main ingredients of an abstract system understanding which in the past decade has successfully served for establishing a formal framework for the system-level design of embedded real-time systems.

The presentation will introduce various methodologies for modelling and analyzing system components with real-time constraints and complying with different computational models. Furthermore it will discusse how the abstract system understanding, as illustrated above, can be exploited for unifying a heterogenous landscape of modelling methodologies and combine them in a single framework, ultimately targeting a rigorously formal and compositional analysis of distributed (hard) real-time systems.

Short Bio:

Kai Lampka received his Diplom-Informatiker and Dr.-Ing. degrees in Computer Science from the Friedrich-Alexander University Erlangen-Nuremberg 2001 and 2007 respectively. During this time, he was working in the group of Prof. Siegle, first at Erlangen (2002-2004) and from 2004 until 2007 at the University of the Federal Forces (Munich). Since 2007 he is a post-doctoral researcher in the computer engineering research group of Prof. Thiele. His domain of expertise is the formal systems verification, i.e., state-based methodologies and their analysis algorithms. He has a background in stochastic performance analysis, i.e., in finite state Markov modelling and Decision Diagram based analysis of high-level Markov model descriptions. Kai Lampka has been awarded with “Best Paper Awards”, at the 13th GI/ITG Conference on Measurement, Modelling and Evaluation of Computer and Communication Systems 2006 (MMB 2006) and at the ACM/SIGBED Embedded System Conference 2009 (EMSOFT 2009).

Date: Tuesday April 19th, 2011, 14.00

Location: Battelle bât A, auditorium ground floor

À la Une