Humboldt-Universität zu Berlin - Faculty of Mathematics and Natural Sciences - Department of Computer Science

Research at the Chair Theory of Programming


Long-term Aim of Research

Informatics presents itself as an engineering discipline. Nevertheless, one may ask for a more comprehensive and basic scientific discipline, comprising a kind of discrete, stepwise proceeding dynamic systems, and focusing on formal, mathematical principles and methods to cover what may be denoted as “information”, together with its use and its handling. Examples for formal concepts of information processing that are not intended to be implemented, include many aspects of business informatics and embedded systems.

Research at the Chair Theory of Programming contributes to the development of this kind of a theoretical basis for a science of informatics.




The Project COMPOSE!

COMPOSE! is a project that contributes to methods to construct adequate models for discrete systems, in particular process driven, computer embedded systems. Such systems are usually quite large and not manageable as monolithic entities. Component technology and service-orientation therefore suggest composing such systems from smaller components. Much discussed micro-services support this paradigm. Business processes, scientific workflows and numerous further areas of applied computer science exhibit similar structures. The advantages of this kind of architecture is obvious: single components can be updated or deleted, new components can be embedded, quests for properties of a system can frequently be reduced to properties of its components and their composition.

A central problem of such structures are adequate, useful, and fitting basic principles to compose components. The COMPOSE! project develops such principles. Case studies demonstrate the use of those principles.

In technical terms, COMPOSE! builds on a conceptually new, generic composition operator for any kind of interface equipped components. First results have been gained, showing breadth and flexibility of the composition operator.


The Project Modeling and Invariance

The core of scientific theories includes models, describing the central items of the respective scientific area. Intuitive explanations, causal dependencies and predictable properties can be derived from those models.

In this project we ask for scientific models for informatics. As usual in science, models are used to describe dynamic behavior of systems. Those systems differ however fundamentally from other sciences: classical physics describes behavior (mostly) continuously, using functions over a real-number time axis. Differential equations, integrals and many more deep mathematical concepts are available in this framework. In contrast, informatics describes behavior in discrete steps. This allows to cover entirely different properties and to use different analysis techniques.

The seamless integration of computers with their organizational or technical environment is fundamental for many embedded systems, not least for the internet of things: such systems are manageable only with models that comprise both, computers and their environment. In particular, this includes models for components that are not intended to be implemented.

Numerous modeling techniques support this aspect, most prominently the UML, and – primarily for business informatics – the BPMN notation. However, these two (and many other) modeling techniques offer very limited analysis techniques. Hence, even if a system is carefully modelled by means of those techniques, correctness can not be guaranteed on the level of the model, but only on the level of its implementation. This reduces decisively the value of modeling.

A really useful theory of informatics would manage correctness on the level of models. From such models, software may be derived that is correct by construction.

This project develops modeling methods with deeply rooted analysis techniques. In particular, liberal and powerful notions of invariants are developed.


Publications from 2019 can be found here.