ACPS: Automating CPS Design

In the "Automating CPS Design" Research group, we develop methods for automating the design process of correct and efficient cyber-physical and embedded systems to the largest possible extent.

In this context, we adress the following research questions:

1. How can we automatically synthesize correct-by-construction systems? - Engineers often spend a lot of time writing down requirements for embedded systems in addition to developing the actual systems. Being able to compute the system from the specification automatically would substantially reduce development time.
2. How can we apply machine learning in embedded systems in a way that the the system satisfies important correctness properties? - Systems that adapt to their environment often profit from the use of machine learning. But without being able to give safety guarantees, such systems are often not usable in the field.
3. How can we make the engineering process of correct and efficient systems more time-efficient in general? - Many moder embedded systems were developed with little regard for their provable correctness, because this is often too expensive. How can we improve this poor state of the art?

At the interface between theory and practice, we research and develop new methods and algorithms to solve these problems. More precisely, we perform research in the following sub-fields of computer science:

• Verification and Quality Assurance of learned artificial neural netoworks
• Reactive Synthesis
• Runtime Verification
• The interaction of embedded systems and formal methods

In our work, we import a lot of concepts from related subfields of computer science, such as satisfiability solving, automata theory, more general formal methods, as well as mathematical optimization. We use these concepts to solve the difficult computational problems that arise in the context of our work.

We also perform resaerch in the scope of third-party funded projects and endeavors, such as:

• GUISynth - Reactive synthesis of program code for graphical user interfaces (DFG)
• SafeWahr - Runtime correctness testing in the concept of autonomous driving (BMWI)
• Formal Engineering Support for Field-Programmable Gate Arrays (Volkswagenstiftung)

Our research often leads to the implementation of our researched concepts and algorithms in the context of (academic) software, such as:

• Slugs: GR(1) Reactive Synthesis Tool
• Planet: Neural Network Verification
• GUISynth: Framework for synthesizing graphical user interface code for Android Cell Phone Apps

We also regularly offer Bachelor's and Master's thesis as well as projects in the scope of the B.Sc. and M.Sc. computer science courses of study at TU Clausthal.