Method for synthesizing a correct-by-construction control software for Advanced Driver Assistance Systems (ADAS)

The number of ADAS features in modern cars increases. Consequently, there is an insisting demand to ensure that all hardware and software components of the car will work as intended. The development of safety-critical functions such as advanced-collision-avoidance or lane-keeping is usually guided by functional safety standards such as the ISO26262 standard. The standard highly recommends that systems classified with Automotive Safety Integrity Levels (ASIL) C and D should utilize formal approaches for defining the requirements, verifying the designs, and/or generating the design/implementation.

This invention presents a novel solution to design certifiable control software for safety-critical systems such as self-driving cars. It provides an approach to automatically generate correct-by-construction control software from given formal requirements. Using the approach in the invention to design a control software (e.g., ADAS function) ensures its correctness and implies that the designed component is formally-verified. This provides a valuable tool for OEMs and T1-Suppliers to include high-ASIL certified ADAS software components in their cars. Unlike all existing approaches of formal verification/design of control software, the invention allows for real-time design, and code-generation, of the formally-correct control software.

Given some formal design requirements that need to be enforced on a system defined by inputs, states and outputs, the invention proposes a method for synthesizing a correct-by-construction control software that is guaranteed to satisfy the design requirements. It is based on a recently introduced methodology known as symbolic control [1]. A symbolic model (directed labeled graph) is first automatically derived from the given system. Then, using the formal design requirements, a controller is extracted algorithmically using graph-theoretic techniques.

Advantages of the invention compared to all state-of-the-art methods are:

1. Faster and highly resource-efficient:the construction of the symbolic model and the synthesis of the controller are both data-parallel algorithms so that the current implementation scales almost linearly on multi-core CPUs and GPUs.

2. Highly scalable, enables even real-time applications: due to 1. the software complexity of the implementation is negatively related to available compute resources. This means that the time needed to find/generate the control software can be reduced almost-linearly by adding more parallel processing elements.

3. Applicable to a large range of control systems: original systems are assumed to be general systems with inputs, states, and outputs. This includes linear/non-linear control systems described by ODEs, discrete-time systems, or even software systems. The authors showcased the invention by implementing a formally-verified path planner for autonomous robots [2].

4. Minimal human interaction: the whole process for designing the control software is automated and the final controller is code-generated, which ensures an error-free and formally-verified final product.

5. Certifiable control software: the invention is based on formal methods for designing and generating the control software, and its final product (i.e., the control software) can be easily certifiable. This is a plus for software/hardware components that must be classified as ASIL C or D.

The invention prevents ambiguity and false implementation. Formalizing and automating the generation of safety-critical control software/hardware helps certifying them (higher ASIL). The invention can be a game changer for automotive OEMs and/or Tier1 automotive software companies in terms of functional safety, development speed and cost.

The technique is already implemented and tested on lab-scale systems in the Technical University of Munich (TUM), Germany, and University of Colorado Boulder (CUB), USA. The implementation can be provided to future patent owners/licensees. Several extensions have been implemented an/or introduced by the inventors after the submission of the patent [3-7]. The implementation effort for the future patent owner/licensee is minimal and only limited to the integration of the implementation of the invention into their specific development or manufacturing process.