-
A Formal-Methods Approach to Provide Evidence in Automated-Driving Safety Cases
Authors:
Jonas Krook,
Yuvaraj Selvaraj,
Wolfgang Ahrendt,
Martin Fabian
Abstract:
The safety of automated driving systems must be justified by convincing arguments and supported by compelling evidence to persuade certification agencies, regulatory entities, and the general public to allow the systems on public roads. This persuasion is typically facilitated by compiling the arguments and the compelling evidence into a safety case. Reviews and testing, two common approaches to e…
▽ More
The safety of automated driving systems must be justified by convincing arguments and supported by compelling evidence to persuade certification agencies, regulatory entities, and the general public to allow the systems on public roads. This persuasion is typically facilitated by compiling the arguments and the compelling evidence into a safety case. Reviews and testing, two common approaches to ensure correctness of automotive systems cannot explore the typically infinite set of possible behaviours. In contrast, formal methods are exhaustive methods that can provide mathematical proofs of correctness of models, and they can be used to prove that formalizations of functional safety requirements are fulfilled by formal models of system components. This paper shows how formal methods can provide evidence for the correct break-down of the functional safety requirements onto the components that are part of feedback loops, and how this evidence fits into the argument of the safety case. If a proof is obtained, the formal models are used as requirements on the components. This structure of the safety argumentation can be used to alleviate the need for reviews and tests to ensure that the break-down is correct, thereby saving effort both in data collection and verification time.
△ Less
Submitted 13 October, 2022;
originally announced October 2022.
-
On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic
Authors:
Yuvaraj Selvaraj,
Jonas Krook,
Wolfgang Ahrendt,
Martin Fabian
Abstract:
Cyber-physical systems are often safety-critical and their correctness is crucial, as in the case of automated driving. Using formal mathematical methods is one way to guarantee correctness. Though these methods have shown their usefulness, care must be taken as modeling errors might result in proving a faulty controller safe, which is potentially catastrophic in practice. This paper deals with tw…
▽ More
Cyber-physical systems are often safety-critical and their correctness is crucial, as in the case of automated driving. Using formal mathematical methods is one way to guarantee correctness. Though these methods have shown their usefulness, care must be taken as modeling errors might result in proving a faulty controller safe, which is potentially catastrophic in practice. This paper deals with two such modeling errors in differential dynamic logic. Differential dynamic logic is a formal specification and verification language for hybrid systems, which are mathematical models of cyber-physical systems. The main contribution is to prove conditions that when fulfilled, these two modeling errors cannot cause a faulty controller to be proven safe. The problems are illustrated with a real world example of a safety controller for automated driving, and it is shown that the formulated conditions have the intended effect both for a faulty and a correct controller. It is also shown how the formulated conditions aid in finding a loop invariant candidate to prove properties of hybrid systems with feedback loops. The results are proven using the interactive theorem prover KeYmaera X.
△ Less
Submitted 12 July, 2022;
originally announced July 2022.
-
Robust Stutter Bisimulation for Abstraction and Controller Synthesis with Disturbance: Proofs
Authors:
Jonas Krook,
Robi Malik,
Sahar Mohajerani,
Martin Fabian
Abstract:
This paper proposes a method to synthesise controllers for cyber-physical systems such that the controlled systems satisfy specifications given as linear temporal logic formulas. The focus is on systems with disturbance, where future states cannot be predicted exactly due to uncertainty in the environment. The approach used to solve this problem is to first construct a finite-state abstraction of…
▽ More
This paper proposes a method to synthesise controllers for cyber-physical systems such that the controlled systems satisfy specifications given as linear temporal logic formulas. The focus is on systems with disturbance, where future states cannot be predicted exactly due to uncertainty in the environment. The approach used to solve this problem is to first construct a finite-state abstraction of the original system and then synthesise a controller for the abstract system. For this approach, the robust stutter bisimulation relation is introduced, which preserves the existence of controllers for any given linear temporal logic formula. States are related by the robust stutter bisimulation relation if the same target sets can be guaranteed to be reached or avoided under control of some controllers, thereby ensuring that disturbances have similar effect on paths that start in related states. This paper presents an algorithm to construct the corresponding robust stutter bisimulation quotient to solve the abstraction problem, and it is shown, by explicit construction, that there exists a controller enforcing a linear temporal logic formula for the original system if and only if a corresponding controller exists for the quotient system. Lastly, the result of the algorithm and the controller construction are demonstrated by application to an example of robot navigation.
△ Less
Submitted 27 May, 2022;
originally announced May 2022.
