ACPS: Automating CPS Design

In the "Automating CPS Design" research group, we develop methods to automate the development process of correct and efficient cyber-physical and embedded systems to the greatest possible extent.

We consider the following main questions:

  1. How can we synthesize correct implementations synthesize? - Engineers often spend a lot of time writing requirements for embedded systems and developing the systems themselves. It would be better if we could generate the system implementations directly from the requirements, as this would save a lot of development time.
  2. How can we use machine learning methods in embedded systems in such a way that they fulfill important correctness properties? - Systems that adapt to their environment in particular benefit enormously from the use of machine learning. But without security guarantees, they often cannot be used.
  3. In general, how can we make it easier for engineers to build correct and efficient systems? - Many of today's embedded systems have been developed with little regard for correctness because this has simply been too expensive up to now. How can we make it cheaper?

At the interface between theory and practice, we are developing new methods and algorithms to solve these problems. To this end, we conduct research in the following sub-topics of computer science:

  • Verification and quality assurance of learned artificial neural networks
  • Reactive synthesis
  • Runtime Verification

In our work, we import many concepts from related areas of computer science, such as machine learning, satisfiability solving, automata theory, more generally formal methods, and also mathematical optimization. One focus is on the use of such concepts to solve the difficult computational problems that arise in our work.

We also conduct our research in the area of third-party funded projects and ventures, such as:

Our research often leads to the implementation of the developed concepts in software, e.g:

  • SlugsGR(1) Reactive Synthesis Tool
  • PlanetNeural Network Verification
  • GUISynth: Framework for synthesizing graphical user interface code for Android Cell Phone Apps

We also regularly offer bachelor and master theses as well as project work on the topics mentioned above.