| 1. |
- Krook, Jonas, 1986
(författare)
-
Correct-by-Construction Tactical Planners for Automated Cars
- 2019
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- One goal of developing automated cars is to completely free people from driving tasks. Automated cars that require no human driver need to handle all traffic situations that a human driver is expected to handle, and possibly more. Although human drivers cause a lot of traffic accidents, they still have a very low accident and failure rate that automated systems must match. Tactical planners are responsible for making discrete decisions during the coming seconds or minute. As with all subsystems in an automated car, these planners need to be supported with a credible and convincing argument of their correctness. The planners' decisions affect the environment and the planners need to interact with other road users in a feedback loop, so the correctness of the planners depend on their behavior in relation to other drivers and the environment over time. One possibility to ascertain their correctness is to deploy the planners in real traffic. To be sufficiently certain that a tactical planner is safe by that methods, it needs to be tested on 255 million miles without having an accident. Formal methods can, in contrast to testing, mathematically prove that the requirements are fulfilled. Hence, they are a promising alternative for making credible arguments of tactical planners' correctness. The topic of this thesis is how formal methods can be used in the automotive industry to design safe tactical planners. What is interesting is both how automotive systems should be modeled in formal frameworks, and how formal methods can be used practically within the automotive development process. The main findings of this thesis are that it is natural to express desired properties of tactical planners in formal languages and use formal methods to prove their correctness. Model Checking, Reactive Synthesis, and Supervisory Control Theory have been used in the design and development process of tactical planners, and all three methods have their benefits, depending on the application. Formal synthesis is an especially interesting class of formal methods because they can automatically generate a planner based on requirements and models. Formal synthesis removes the need to manually develop and implement the planner, so the development efforts can be directed to formalizing good requirements on the planner and good assumptions on the environment. However, formal synthesis has two limitations: the resulting planner is a black box that is difficult to inspect, and it is difficult to find a level of abstraction that allows detailed requirements and generic planners.
|
|
| 2. |
- Krook, Jonas, 1986, et al.
(författare)
-
Design and Formal Verification of a Safe Stop Supervisor for an Automated Vehicle
- 2019
-
Ingår i: Proceedings - IEEE International Conference on Robotics and Automation. - : Institute of Electrical and Electronics Engineers (IEEE). - 1050-4729. - 9781538660263 ; 2019-May, s. 5607-5613
-
Konferensbidrag (refereegranskat)abstract
- Autonomous vehicles apply pertinent planning and control algorithms under different driving conditions. The mode switch between these algorithms should also be autonomous. On top of the nominal planners, a safe fallback routine is needed to stop the vehicle at a safe position if nominal operational conditions are violated, such as for a system failure. This paper describes the design and formal verification of a supervisor to manage all requirements for mode switching between nominal planners, and additional requirements for switching to a safe stop trajectory planner that acts as the fallback routine. The supervisor is designed via a model-based approach and its abstraction is formally verified by model checking. The supervisor is implemented and integrated with the Research Concept Vehicle, an experimental research and demonstration vehicle developed at the KTH Royal Institute of Technology. Simulations and experiments show that the vehicle is able to autonomously drive in a safe manner between two parking lots and can successfully come to a safe stop upon GPS sensor failure.
|
|
| 3. |
- Krook, Jonas, 1986
(författare)
-
Formal Methods and Safety for Automated Vehicles: Modeling, Abstractions, and Synthesis of Tactical Planners
- 2022
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- One goal of developing automated road vehicles is to completely free people from driving tasks. Automated vehicles with no human driver must handle all traffic situations that human drivers are expected to handle, possibly more. Though human drivers cause a lot of traffic accidents, they still have a very low accident and failure rate that automated vehicles must match. Tactical planners are responsible for making discrete decisions for the coming seconds or minutes. As with all subsystems in an automated vehicle, these planners need to be supported with a credible and convincing argument of their correctness. The planners interact with other road users in a feedback loop, so their correctness depends on their behavior in relation to other drivers and road users over time. One way to ascertain their correctness is to test the vehicles in real traffic. But to be sufficiently certain that a tactical planner is safe, it has to be tested on 255 million miles with no accidents. Formal methods can, in contrast to testing, mathematically prove that given requirements are fulfilled. Hence, these methods are a promising alternative for making credible arguments for tactical planners’ correctness. The topic of this thesis is the use of formal methods in the automotive industry to design safe tactical planners. What is interesting is both how automotive systems can be modeled in formal frameworks, and how formal methods can be used practically within the automotive development process. The main findings of this thesis are that it is viable to formally express desired properties of tactical planners, and to use formal methods to prove their correctness. However, the difficulty to anticipate and inspect the interaction of several desired properties is found to be an obstacle. Model Checking, Reactive Synthesis, and Supervisory Control Theory have been used in the design and development process of tactical planners, and these methods have their benefits, depending on the application. To be feasible and useful, these methods need to operate on both a high and a low level of abstraction, and this thesis contributes an automatic abstraction method that bridges this divide. It is also found that artifacts from formal methods tools may be used to convincingly argue that a realization of a tactical planner is safe, and that such an argument puts formal requirements on the vehicle’s other subsystems and its surroundings.
|
|
| 4. |
- Krook, Jonas, 1986, et al.
(författare)
-
Formal Synthesis of Safe Stop Tactical Planners for an Automated Vehicle
- 2020
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 53:4, s. 445-452
-
Konferensbidrag (refereegranskat)abstract
- Automated vehicles need a safe back-up solution in the presence of system degradations since a driver cannot be expected to take control on short notice. In the event of a degradation, the vehicle is required to reach a minimal risk condition via a minimal risk maneuver. The activation of such maneuvers is safety critical, and a correct implementation of the tactical planner that takes the activation decision is paramount. One way to ensure correctness is to employ formal methods since they can provide proofs thereof. Earlier, a tactical planner was formally verified to activate a minimal risk maneuver if and only if a failure occurs. Formal verification has some drawbacks, so this paper investigates the applicability of using the tools Supremica and TuLiP to synthesize correct-by-construction tactical planners. These two tools amend some of the verification’s drawbacks, but also introduce their own.
|
|
| 5. |
- Krook, Jonas, 1986, et al.
(författare)
-
Modeling and Synthesis of the Lane Change Function of an Autonomous Vehicle
- 2018
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 51:7, s. 133-138
-
Konferensbidrag (refereegranskat)abstract
- Unexpected incorrect behavior of autonomous vehicles can have catastrophic outcomes. But, as with any large-scale software development, correctness of the system is not easily guaranteed. As the system is made up of multiple sub-modules that interact with each other, unexpected behavior can arise from incorrect interactions between the modules. In a previous paper, formal verification was applied to the lane change module of the decision and control software (under development) for an autonomous vehicle. This revealed incorrectness in the model, which could also be shown to exist in the actual software. Manual changes to the model did not result in absence of the incorrectness, and so in this paper we aim to patch the error by applying synthesis. The synthesized result is correct by construction, but it is not obvious what part of the functionality is disabled by the synthesis. Though different synthesis techniques were able to generate supervisors for the model, only when the supervisor was expressed as guard conditions on the events was it possible to interpret the effect of the synthesis. However, the supervisors put constraints on how the input data to the lane change module might change, so in the end the supervisors put behavioral requirements on the modules that generate the input to the lane change module.
|
|
| 6. |
- Krook, Jonas, 1986, et al.
(författare)
-
Robust stutter bisimulation for abstraction and controller synthesis with disturbance
- 2024
-
Ingår i: Automatica. - 0005-1098. ; 160
-
Tidskriftsartikel (refereegranskat)abstract
- This paper proposes a method to synthesise controllers for cyber-physical systems subjected to disturbances, such that the controlled system satisfies specifications given as linear temporal logic formulas. To solve this problem, a finite-state abstraction of the original system is first constructed, and then a controller is synthesised for the abstraction. Due to the disturbances and uncertainty in the environment, future states cannot be predicted exactly, and the abstraction must take this into account. For this purpose, the robust stutter bisimulation relation is introduced, which preserves the existence of controllers for any given linear temporal logic formula that excludes the next operator. 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 controller, thus ensuring that disturbances have similar effect on paths that start in related states. It is shown that there exists a controller enforcing a linear temporal logic formula for the original system if and only if a controller exists for the abstracted system. The approach is illustrated by a robot navigation example.
|
|
| 7. |
- Krook, Jonas, 1986, et al.
(författare)
-
Robust Stutter Bisimulation for Abstraction and Controller Synthesis with Disturbance: Proofs
- 2022
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)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 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.
|
|
| 8. |
- Ramezani, Zahra, 1988, et al.
(författare)
-
Comparative Case Studies of Reactive Synthesis and Supervisory Control
- 2019
-
Ingår i: 2019 18th European Control Conference, ECC 2019. ; , s. 1752-1759
-
Konferensbidrag (refereegranskat)abstract
- Reactive Synthesis and Supervisory Control Theory are both systematic approaches for the automatic construction of controllers from requirements. However, their underlying technicalities differ significantly. This paper provides an empirical comparison between these two approaches from the modelling perspective through case studies. Using the synthesis tools TuLiP and Supremica, two examples are modelled in the typical modelling formalism supported by each tool, and the algorithms are applied to synthesize controllers. Based on the obtained models and experiences, we compare how the models are derived, and how the characteristics of the examples and the underlying synthesis algorithms influence the modelling choices.
|
|
| 9. |
- Selvaraj, Yuvaraj, 1990, et al.
(författare)
-
On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic
- 2022
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 13478, s. 281-297
-
Konferensbidrag (refereegranskat)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 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.
|
|
| 10. |
- Selvaraj, Yuvaraj, 1990, et al.
(författare)
-
On proving that an unsafe controller is not proven safe
- 2024
-
Ingår i: Journal of Logical and Algebraic Methods in Programming. - 2352-2208 .- 2352-2216. ; 137
-
Tidskriftsartikel (refereegranskat)abstract
- Cyber-physical systems are often safety-critical and their correctness is crucial, such as in the case of automated driving. Using formal mathematical methods is one way to guarantee correctness and improve safety. Although these methods have shown their usefulness, care must be taken because modelling errors might result in proving a faulty controller safe, which is potentially catastrophic in practice. This paper deals with two such modelling errors in differential dynamic logic, a formal specification and verification language for hybrid systems, which are mathematical models of cyber-physical systems. The main contributions are to provide conditions under which these two modelling errors cannot cause a faulty controller to be proven safe, and to show how these conditions can be proven with help of the interactive theorem prover KeYmaera X. 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. Furthermore, the relation between such a loop invariant and the characterisation of the maximal control invariant set is discussed.
|
|
