Safe Integration of Learning In Autonomous cyber-physical Systems (Safe ILIAS)

信息物理系统是将联合收割机离散控制（或信息）方面与物理方面相结合的系统。我们可以在汽车、飞机或供水系统中找到这种系统的例子。随着当前自动驾驶汽车和智能基础设施的发展趋势，这些系统正变得越来越自主。这意味着他们可以利用学习在不可预见的情况和动态环境中做出良好的控制决策。虽然学习大大增加了他们的灵活性，但也增加了他们的复杂性。与此同时，网络物理系统的故障往往会造成严重后果，因为它们可能造成巨大的经济损失甚至生命损失。因此，这些系统的正确性和可靠性至关重要。形式化验证技术使用严格的数学方法来确定正确性，可以为我们提供有关网络物理系统关键安全属性的保证。然而，众所周知，正式验证是非常昂贵的。用于自动验证的技术探索给定系统的底层状态空间，其通常太大而不能完全探索。演绎验证技术通过利用抽象的数学推理为这个问题提供了一个强大的解决方案，但它们需要巨大的努力和专业知识来提供必要的抽象和证明思想来指导验证过程。这个问题对于自主网络物理系统来说尤其严重，因为学习中常用的试错过程和统计方法很难被正式捕获。这个项目的主要目标是在自主网络物理系统中安全地集成学习，并做出可接受的努力。我们实现这一目标的关键概念是可重用性。特别是，我们调查可重用的抽象自主网络物理系统。通过为正式规范和抽象（例如，属性和规范模式）的系统重用提供新的概念，我们将显著减少所需的手动工作和专业知识，从而提高演绎验证在自主网络物理系统的工业设计过程中的适用性和接受度。

Cyber-physical systems are systems that combine discrete control (or cyber) aspects with physical aspects. We can find examples of such systems in cars, airplanes, or water supply systems. With the current trend towards self-driving cars and smart infrastructures, these systems are becoming increasingly autonomous. This means that they use learning to take good control decisions in unforeseen situations and dynamic environments. While learning significantly increases their flexibility, it also increases their complexity. At the same time, failures often have serious consequences in cyber-physical systems, as they may cause huge financial losses or even loss of lives. Thus, the correctness and reliability of these systems are of vital importance. Formal verification techniques, which establish correctness using rigorous mathematical methods, can provide us with guarantees about crucial safety properties of cyber-physical systems. However, formal verification is known to be enormously expensive. Techniques for automatic verification explore the underlying state space of a given system, which is often too large to be fully explored. Deductive verification techniques provide a powerful solution to this problem by leveraging abstract mathematical reasoning, but they require tremendous effort and expertise to provide the necessary abstractions and proof ideas to guide the verification process. This problem is especially severe for autonomous cyber-physical systems, because the trial-and-error processes and statistical methods that are commonly used in learning are hard to capture formally.The main goal of this project is the safe integration of learning in autonomous cyber-physical systems with acceptable effort. Our key concept to achieve this is reusability. In particular, we investigate reusable abstractions for autonomous cyber-physical systems. By providing novel concepts for systematic reuse of formal specifications and abstractions (for example, property and specification patterns), we will significantly reduce the required manual effort and expertise, and thus increase the applicability and acceptance of deductive verification in industrial design processes for autonomous cyber-physical systems.