The open and cooperative nature of Cyber-Physical Systems (CPS) poses a significant new challenge in assuring dependability. The DEIS project addresses this important and unsolved challenges by developing technologies that form a science of dependable system integration. In the core of these technologies lies the concept of a Digital Dependability Identity (DDI) of a component or system. DDIs are composable and executable in the field facilitating (a) efficient synthesis of component and system dependability information over the supply chain and (b) effective evaluation of this information in-the-field for safe and secure composition of highly distributed and autonomous CPS.

In safety-critical systems miscompilation is a serious problem since it can cause erroneous or erratic behavior including memory corruption and program crash, which may manifest sporadically and often is hard to identify and track down. Many verification activities are performed at the architecture, model, or source code level, but all properties demonstrated there may not be satisfied at the executable code level when miscompilation happens. This is not only true for source code review but also for formal, tool-assisted verification methods such as static analyzers, deductive verifiers, and model checkers. In consequence, many safety standards require additional, difficult and costly verification activities to show that the requirements already shown at higher levels are also satisfied at the executable object code level. CompCert is an optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. We give an overview of the design of CompCert and its proof concept and then focus on aspects relevant for industrial application. We summarize practical experience and give an overview of recent CompCert development aiming at industrial usage. CompCert’s intended use is the compilation of life-critical and mission-critical software meeting high levels of assurance. In this context tool qualification is of paramount importance. We summarize the confidence argument of CompCert and give an overview of qualification strategies.

Algorithms incorporating learned functionality play an increasingly important role for highly automated vehicles. Despite their impressive performance for cognitive tasks such as environmental perception, their verification within a safety analysis remains one of the most challenging tasks within the development process. We propose to integrate known statistical guarantee statements about the generalization ability from individual data points with the functional architecture as well as constraints about the dynamics and ontology of the physical world, which allows us to (a) formulate and solve a safety verification problem of architectures using artificial intelligence components and (b) to understand traditional safety mechanisms as a bridge over the gap between performance of perception sub-systems and safety of the overall driving function.

Die Automobilindustrie steht im Zuge der Entwicklung des automatischen Fahrens vor vollkommen neuartigen Herausforderungen: insbesondere das autonome Fahren Level 5 hat erhöhte Anforderungen im Bereich der Zuverlässlichkeit, Verfügbarkeit und Widerstandsfähigkeit an das Fahreugsystem, da im Fehlerfall der Fahrer als Rückfallebene nicht mehr zur Verfügung steht.
Außerdem werden klassische modellgetriebene Verfahren zunehmend von datengetriebenen Verfahren abgelöst, was wiederum neue Herausforderungen in der Safety Absicherung schafft.
In diesem Vortrag werden diese Herausforderungen sowie sich daraus ergebenen Veränderungen im Entwicklungsprozess aufgezeichnet.

Control design and verification of cyber-physical systems are challenging problems, due to mixed discrete and continuous dynamics, unreliable sub-systems and complex environments. Connected, automated vehicles exemplify these properties in huge numbers of time-varying environmental variables, non-deterministic continuous dynamics, interactions with non-communicating vehicles and unreliable wireless communication with other automated vehicles. In the project UnCoVerCPS we investigate a toolchain for unification of control and verification of cyber-physical systems and apply these techniques to cooperative, automated driving. Thereby complementing classical testing with online-verification techniques. During operation of an automated vehicle, a supervisory module verifies possible actions that are proposed by high-level control processes. These actions are evaluated under the assumption of certain worst-case behaviors of other traffic participants, non-deterministic sensors and actuators, as well as past agreements with other communicating, automated vehicles. By switching between desired actions and emergency maneuvers, the supervisor guarantees invariant safety of its vehicle. Through the combination of offline and online verification steps, we can incorporate detailed models of the environment, of the vehicle and the behavior of other traffic participants. Furthermore, we make no restrictive assumptions about the control modules that propose actions to the supervisor. Thus, complex and adaptive controllers, (e.g. machine learning based techniques), can be integrated into the safety concept. We present intermediate project results, including physical test drives and real-time simulation and discuss implications and benefits of the proposed concept.