Foundations of
Perspicuous Software Systems

Collaborative Research Center 248

:doodle {@grid: 3 / 25em;} background: hsla(0, calc(90% + 10%/@index()), calc(99% + 1%/@index()), @rand(0.0, 0.7, .1)); transform: scale(@rand(.2, .9)); transform: rotate(@r(@rand(0, 360)deg)); @shape: rectangle; animation: scale-up 15s linear infinite; animation-delay: calc(@i() * -.6s); @keyframes scale-up { 0% { opacity: @rand(0, 1); transform: scale(@rand(0.01, 0.2)); } 50% { opacity: @rand(0, 1); transform: scale(@rand(1.2, 2.2)); } 100% { opacity: @rand(0, 1); transform: scale(@rand(0.01, 0.2)); } }
:doodle { @grid: 1/ 10em; } transform: translate(@rand(-100, 100)px, @rand(-100, 100)px); border-color: #569CEF; border-style: solid; border-width: 7px; animation: scale-up 20s linear infinite; animation-delay: calc(@i() * -40s); @keyframes scale-up { 0% { opacity: calc(0+0.8/@index()); transform: scale(@rand(0.3, 0.5)); } 25% { transform: translate(@rand(-150, 150)px, @rand(-150, 150)px); } 60% { transform: translate(@rand(-150, 150)px, @rand(-150, 50)px) scale(@rand(0.8, 1.1)); } 100% { transform: scale(@rand(0.3, 0.5)); opacity: calc(0+0.8/@index()); } }

About

The Transregional Collaborative Research Centre 248 „Foundations of Perspicuous Software Systems“ aims at enabling comprehension in a cyber-physical world with the human in the loop.

From autonomous vehicles to Industry 4.0, from smart homes to smart cities – increasingly computer programs participate in actions and decisions that affect humans. However, our understanding of how these applications interact and what is the cause of a specific automated decision is lagging far behind. With the increase in cyber-physical technology impacting our lives, the consequences of this gradual loss in understanding are becoming severe. Systems lack support for making their behaviour plausible to their users. And even for technology experts it is nowadays virtually impossible to provide scientifically well-founded answers to questions about the exact reasons that lead to a particular decision, or about the responsibility for a malfunctioning. The root cause of the problem is that contemporary systems do not have any built-in concepts to explicate their behaviour. They calculate and propagate outcomes of computations, but are not designed to provide explanations. They are not perspicuous.

The key to enable comprehension in a cyber-physical world is a science of perspicuous computing.

perspicuous /pəˈspɪkjʊəs/
adjective formal
clearly expressed and easily understood; lucid.
able to give an account or express an idea clearly.

Partners
Two excellent locations.

CRC 248 joins the scientific forces at Saarbrücken and Dresden to master the perspicuity challenge. It comprises experts at Technische Universität Dresden and at Saarland Informatics Campus – Universität des Saarlandes, Max Planck Institute for Informatics, and Max Planck Institute for Software Systems.

With CRC 248, the participating institutions establish a transregional network of experts in perspicuous cyber-physical systems. It will serve our society in its need to stay in well-informed control over the computerised systems we all interact with. It enables comprehension in a cyber-physical world.

 

Partners
Two excellent locations.

CRC 248 joins the scientific forces at Saarbrücken and Dresden to master the perspicuity challenge. It comprises experts at Technische Universität Dresden and at Saarland Informatics Campus – Universität des Saarlandes, Max Planck Institute for Informatics, and Max Planck Institute for Software Systems.

With CRC 248, the participating institutions establish a transregional network of experts in perspicuous cyber-physical systems. It will serve our society in its need to stay in well-informed control over the computerised systems we all interact with. It enables comprehension in a cyber-physical world.

 

Our Projects

Project Group C:
Construct

C1: Programming Abstractions for Cyber-Physical Systems

This project develops programming abstractions for cyber-physical applications, together with reasoning and verification techniques for correctness, with synthesis techniques across continuous and discrete phenomena, and with immersive interaction tools visualising data streams for better programmer productivity and comprehension. Our vision is an integrated development environment for programming, verifying, and understanding high- performance and scalable applications perceiving and acting in the physical world. Project C1 is designated to evolve into an integration project for the diverse methods, techniques and tools developed in this CRC addressing perspicuity at design time.

Principal Investigators: R. Majumdar, B. Finkbeiner, S. Gumhold

C2: Composition and Abstraction with Explications

Faithful models of embedded devices need to encompass aspects of time, costs, resource consumption, randomness, continuous dynamics, and uncertainty. These aspects are notoriously difficult to take care of when constructing systems from components. This project aims at establishing and exploiting the principles of composition and abstraction to arrive at an effective cause-effect analysis framework. It revolves around quantitative summaries of component characteristics, together with effective support for compositional analysis, and supported by abstract argumentation for explications.

Principal Investigators: H. Hermanns, C. Baier, S. Gaggl

C3: Supervision of Dynamic Dependable Systems

Future cyber-physical systems are expected to be adaptable in the field without sacrificing dependable operation. This project looks into ways to enable the immediate deployment of new software variants but without risking safety violations. We propose a supervisor-based architecture where the supervisor solicits explications from individual components, and cross-checks these with explications by other, possibly redundant, components. It plans and executes micro-experiments to identify faulty components and to exercise new software variants. It verifiably excludes faulty behaviour once identified. Project C3 is designated to evolve into an integration project for the CRC’s methods addressing perspicuity at run time.

Principal Investigators: C. Fetzer, H. Hermanns, J. Hoffmann

C4: Distributed Knowledge and Information Flow

The focus of this project are cyber-physical systems whose behaviour is described in terms of their distributed knowledge and information flow. These notions localize the decision processes and appeal to the intuition of system components as intelligent agents. We develop the foundational concepts, algorithmic methods, and visualisation tools for a computer-aided construction process where the agent decisions are characterised by the agent’s knowledge as it evolves over time. Our techniques will identify requirements and construct implementations that together are guaranteed to provide the necessary information flow between interacting systems, and – in the long term – in human-system interactions.

Principal Investigators: B. Finkbeiner, M. Krötzsch, R. Dachselt

C5: Combining Program Analysis and Run-Time Monitoring

This project aims to improve understandability of erroneous behaviour in cyber-physical systems using program analysis. Toward this, first, we will establish the fundamental techniques for leveraging concrete information from run-time monitoring of these software systems in order to predict failures with a fast static analysis. We will also investigate the degree of fault tolerance based on run-time speculation. Second, we will tune static analysers to cyber-physical software using run-time information, increasing the detection of true bugs and reducing false alarms, and improving the understandability of program analysis results to users through software-level explications for any detected code issues.

Principal Investigators: M. Christakis, C. Fetzer

C6: Fast, Safe, and Perspicuous Run-Time Planning

Run-time planning serves flexible decision making in dynamic environments. To do so under time pressure, a trained action policy such as a deep neural network can be employed. Our mission is to help tackle the perspicuity and safety issues arising in this context. Among others, we will safeguard the action policy via run-time lookahead search, and by exploiting synergies with design-time analysis; we help to debug the policy via static and dynamic analyses of the behaviours it induces; and we support human understanding of policies through zoomable visualisations. We will advance techniques for search, predicate abstraction, and supervised learning to these ends.

Principal Investigators: J. Hoffmann, M. Christakis, M. Hein

Project Group A:
Analyse & Explicate

A1: Analysing and Explicating Dynamical and Hybrid Systems

Dynamical and hybrid automata models are at the core of operational representations of cyber-physical systems. The vision of the project is to provide an algorithmic analysis framework for these models, together with corresponding explication mechanisms. While the majority of existing methods for dynamical and hybrid systems rely either on semi-algorithms (without termination guarantees) or on approximation techniques (without guarantees of the correctness of the analysis results), the focus of the project will be on the development of provably correct and terminating exact verification algorithms and corresponding techniques for the generation of certificates for verified system properties.

Principal Investigators: J. Ouaknine, C. Baier

A2: Probabilistic Causality and Explications

The project will lay the foundations for a causality-based system analysis as well as the generation of explications that rely on formal cause-effect relations. This analysis supports the understanding of causal chains and of the induced cascades of dependencies between system components at design time, but also the generation of plausibilisations of observed behaviours at run-time. The research program includes algorithmic and complexity- theoretic problems for different forms of causality-based reasoning in stochastic operational models. It will support the transfer of causal structures explicating observations formally to visual or verbal representations explaining them intuitively

Principal Investigators: C. Baier, B. Finkbeiner, R. Majumdar

A3: Description Logic Explications

We will develop sophisticated techniques for the user-adaptive explication of knowledge-based reasoning and its combination with explication generators developed in other projects. We will address explications for the results of description logic reasoners in terms of proofs that a consequence is indeed deducible from a knowledge base, counter-interpretations for non-consequences, as well as visualisations thereof. User groups we will address are knowledge and system engineers as well as layperson users. We will study the combination of explication approaches for description logic reasoning with ones for temporal and probabilistic reasoning.

Principal Investigators: F. Baader, S. Borgwardt, A. Krüger, C. Weidenbach

A4: Logic-Based Perspicuous Run-Time Supervision

This project investigates perspicuous supervision in a read data–analyse–react loop (RAR loop) carried out several times per second within a device, such as an engine control unit. Our vision is a supervisor implemented by logical rules, where (i) the declarative representation and logical reasoning provides explications, turning what nowadays is a black box into a perspicuous system; (ii) testing can be replaced by automatic verification; and (iii) the verified clauses can be deployed within the RAR loop. To these ends, we will investigate the combination of first-order logic fragments representing control aspects with arithmetic theories representing abstractions of physical system behaviour.

Principal Investigators: C. Weidenbach, C. Fetzer, M. Krötzsch

A5: Operational Explications of Classifier Predictions

We develop an explication framework for machine learning techniques with a particular focus on neural networks. As current classifiers are extremely brittle, we will work on provable robustness of the classifier decisions. For such robust classifiers we will provide operational explications presenting to the user how the input would have to change so that the classifier changes its decision, giving priority to slight changes in input. We will investigate efficient visualisation and presentation of the results, aiming at an interactive process exploring operational explications in the neighbourhood of the original input, supporting users in plausibilising the classifier decision, and supporting experts in machine learning when debugging.

Principal Investigators: M. Hein, S. Gumhold

Project Group E:
Explain & Interact

E1: Interactive Exploration of Visual Models

Graph visualisations can present both structural information and multivariate data attributes as a basis for improved understanding and explanation of models of cyber-physical systems. This project aims at enabling the exploration and refinement of models at both design time and inspection time through interactive, responsive visualisation using novel display setups. We identify, design and evaluate suitable representations of models in different complexity and size and develop matching interaction techniques to explore these models as appropriate for the current user, task and context as well as display properties and capabilities, to enable a drastically improved, collaborative model exploration & refinement process.

Principal Investigators: R. Dachselt, F. Baader

E2: Safe Handover in Mixed-Initiative Control

Our mission is to better understand how machines can safely hand over control to humans in mixed-initiative control, and to develop technical support. We will use description logics and planning techniques to characterise situations where a handover is necessary, and to increase the advance notice for handovers at run time. We will combine methods from human-computer interaction and natural language generation to develop solutions for safe and smooth handovers, in particular explaining the relevant situation aspects effectively to the user. Ultimately, we strive to make human aspects of the human-machine system more accessible to formal analysis, thereby ensuring operational safety.

Principal Investigators: A. Krüger, S. Borgwardt, V. Demberg, J. Hoffmann

E3: Knowledge-Driven Inspection

We will establish methods and tools that enable information integration and analysis of cyber-physical systems behaviour at inspection time, based on logical models in expressive rule languages. The project brings together three research areas – logical modelling languages, data-driven reasoning, and adaptive user experience – in order to deliver theoretical insights as well as workable systems. Increased logical expressivity and conflict resolution mechanisms based on abstract argumentation will be integrated into a highly scalable reasoner. The reasoning back-end will be complemented by a front-end for modelling and inspection, whose design is driven by user- experience studie

Principal Investigators: M. Krötzsch, S. Gaggl, A. Krüger

E4: Immersive Analysis of Cyber-Physical Systems

For the inspection of CPS failures, one needs analysis techniques for heterogeneous data that has been recorded from complex processes in the three-dimensional physical world. This project develops augmented reality and virtual reality solutions for intuitive immersive data analysis in a virtual environment. For this, we investigate immersive visualisation and interaction techniques for three-dimensional trajectory data, paired with immersive information visualisation techniques. We will develop a software framework tailored to inspection-time analysis needs. Project E4 is designated to evolve into an integration project for those methods of the CRC addressing perspicuity at inspection time.

Principal Investigators: S. Gumhold, R. Dachselt

Principal
Investigators

CRC 248 is organized into three project groups and led by 18 Principal Investigators.

Prof. Dr.-Ing. Holger Hermanns

Spokesperson
Universität des Saarlandes

Prof. Dr.-Ing. Raimund Dachselt

Co-Spokesperson
Technische Universität Dresden

Prof. Dr.-Ing. Franz Baader

Technische Universität Dresden

Dr.-Ing. Stefan Borgwardt

Technische Universität Dresden

Prof. Christof Fetzer, Ph.D.

Technische Universität Dresden

Dr. Sarah Gaggl

Technische Universität Dresden

Prof. Dr. Matthias Hein

Universität Tübingen

Prof. Dr. Markus Krötzsch

Technische Universität Dresden

Prof. Rupak Majumdar, Ph.D.

Max Planck Institute for Software Systems

Prof. Dr. Christoph Weidenbach

Max Planck Institute for Informatics

Prof. Dr. Christel Baier

Technische Universität Dresden

Dr. Maria Christakis

Max Planck Institute for Software Systems

Prof. Vera Demberg, Ph.D.

Saarland University

Prof. Bernd Finkbeiner, Ph.D.

Saarland University

Prof. Dr. Jörg Hoffmann

Saarland University

Prof. Dr. Antonio Krüger

Saarland University

Prof. Dr. Stefan Gumhold

Technische Universität Dresden

Prof. Joël Ouaknine, Ph.D.

Max Planck Institute for Software Systems

We have open positions
in Perspicuous Computing!

In order to achieve our challenging objectives we are looking for highly motivated researchers who are interested in joining the existing CRC team. We offer 25+ positions in different research areas across computer science comprising, but not limited to, formal methods, artificial intelligence, visualization and human computer interaction. Most of the vacancies are reserved for young researchers aiming at obtaining a PhD degree, but some positions will also be open for postdocs.

Details on the positions available will be published here in the coming weeks. Please stay tuned, or contact jobs@perspicuous-computing.science rightaway.

Contact

Foundations of Perspicuous Software Systems
Enabling Comprehension in a Cyber-Physical World

Transregional Collaborative Research Centre 248 funded by the DFG
An Initiative joining Computer Scientists at Saarland Informatics Campus
and at Technische Universität Dresden

Email: mail@perspicuous-computing.science

Legal Notice
Data protection