RUNTIME MONITORING. AUTOMATIC PROGRAMMING OF RELIABLE SYSTEMS.
Automated systems, such as autopilots, unmanned aircraft systems, and self-driving cars are of increasing interest for a wide range of applications such as logistics, disaster recovery, and public transportation. The stability and security of these systems is critical for the safety of its operating environment. With system health verification, we ensure that every aspect of the system, from sensor data to autonomous decision-making, is either provably correct or supervised during runtime. We develop techniques that enact countermeasures before accidents happen.
Runtime Monitoring of Cyber-Physical Systems Cyber-Physical Systems (CPS), such as medical devices and drones, continuously interact with their unpredictable environment. During runtime, such systems often deal with enormous uncertainty. The reason that CPS fail is often not because of implementation errors or human errors, but because of unforeseen events that occur during operation. With runtime monitoring of CPS we enforce safety limitations on operational aspects, which decrease the risk of failing.
Automatic Programming of Reliable Systems Security vulnerabilities are always very subtle and hidden deeply in many layers of code. For example, insecure information-flow, like a potential leak of credit card information, is often difficult to detect for the human programmer. With automated programming, a computer, instead of a human, implements the desired security mechanisms in the system. We develop techniques and tools that automatically design reliable systems.
Towards Formal Certification We construct concise and complete mathematical models of systems that interact safely and securely in an unpredictable environment. Based on these models, we certify the behaviour of each component, such as the sensor drivers or the flight control in an unmanned aircraft system. We develop a complete tool box for the formal certification of such systems.
