| 1. |
- Huck, Tom P., et al.
(författare)
-
Hazard Analysis of Collaborative Automation Systems: A Two-layer Approach based on Supervisory Control and Simulation
- 2023
-
Ingår i: Proceedings - IEEE International Conference on Robotics and Automation. - 1050-4729. ; 2023-May, s. 10560-10566
-
Konferensbidrag (refereegranskat)abstract
- Safety critical systems are typically subjected to hazard analysis before commissioning to identify and analyse potentially hazardous system states that may arise during operation. Currently, hazard analysis is mainly based on human reasoning, past experiences, and simple tools such as checklists and spreadsheets. Increasing system complexity makes such approaches decreasingly suitable. Furthermore, testing-based hazard analysis is often not suitable due to high costs or dangers of physical faults. A remedy for this are model-based hazard analysis methods, which either rely on formal models or on simulation models, each with their own benefits and drawbacks. This paper proposes a two-layer approach that combines the benefits of exhaustive analysis using formal methods with detailed analysis using simulation. Unsafe behaviours that lead to unsafe states are first synthesised from a formal model of the system using Supervisory Control Theory. The result is then input to the simulation where detailed analyses using domain-specific risk metrics are performed. Though the presented approach is generally applicable, this paper demonstrates the benefits of the approach on an industrial human-robot collaboration system.
|
|
| 2. |
- Selvaraj, Yuvaraj, 1990, et al.
(författare)
-
Automatically Learning Formal Models: An Industrial Case from Autonomous Driving Development
- 2020
-
Ingår i: Proceedings of the ACM/IEEE Joint Conference on Digital Libraries. - New York, NY, USA : ACM. - 1552-5996.
-
Konferensbidrag (refereegranskat)abstract
- The correctness of autonomous driving software is of utmost importance as incorrect behaviour may have catastrophic consequences. Though formal model-based engineering techniques can help guarantee correctness, challenges exist in widespread industrial adoption. One among them is the model construction problem. Manual construction of formal models is expensive, error-prone, and intractable for large systems. Automating model construction would be a great enabler for the use of formal methods to guarantee software correctness and thereby for safe deployment of autonomous vehicles. Such automated techniques can be beneficial in software design, re-engineering, and reverse engineering. In this industrial case study, we apply active learning techniques to obtain formal models from an existing autonomous driving software (in development) implemented in MATLAB. We demonstrate the feasibility of active automata learning algorithms for automotive industrial use. Furthermore, we discuss the practical challenges in applying automata learning and possible directions for integrating automata learning into automotive software development workflow.
|
|
| 3. |
- Selvaraj, Yuvaraj, 1990, et al.
(författare)
-
Automatically Learning Formal Models from Autonomous Driving Software
- 2022
-
Ingår i: Electronics (Switzerland). - : MDPI AG. - 2079-9292. ; 11:4
-
Tidskriftsartikel (refereegranskat)abstract
- The correctness of autonomous driving software is of utmost importance, as incorrect behavior may have catastrophic consequences. Formal model-based engineering techniques can help guarantee correctness and thereby allow the safe deployment of autonomous vehicles. However, challenges exist for widespread industrial adoption of formal methods. One of these challenges is the model construction problem. Manual construction of formal models is time-consuming, error-prone, and intractable for large systems. Automating model construction would be a big step towards widespread industrial adoption of formal methods for system development, re-engineering, and reverse engineering. This article applies active learning techniques to obtain formal models of an existing (under development) autonomous driving software module implemented in MATLAB. This demonstrates the feasibility of automated learning for automotive industrial use. Additionally, practical challenges in applying automata learning, and possible directions for integrating automata learning into the automotive software development workflow, are discussed.
|
|
| 4. |
- Chandru, Rajashekar, 1991, et al.
(författare)
-
Safe autonomous lane changes in dense traffic
- 2017
-
Ingår i: IEEE International Conference on Intelligent Transportation Systems-ITSC. - 2153-0009. - 9781538615263 ; 2018-March
-
Konferensbidrag (refereegranskat)abstract
- Lane change manoeuvres are complex driving manoeuvres to automate since the vehicle has to anticipate and adapt to intentions of several surrounding vehicles. Selecting a suitable gap to move/merge into the adjacent lane and performing the lane change can be challenging, especially in dense traffic. Existing gap selection methods tend to be either cautious or opportunistic, both of which directly affect the overall availability and safety of the autonomous feature. In this paper we present a method which enables the autonomous vehicles to increase the availability of lane change manoeuvres by reducing the required margins to ensure a safe manoeuvre. The required safety margins are first calculated by making use of the steering and braking capability of the vehicle. It is then shown that this method can be used to perform autonomous lane changes in dense traffic situations with small inter-vehicle gaps. The proposed solution is evaluated by using Model Predictive Control (MPC) to plan and execute the complete motion trajectory.
|
|
| 5. |
- Selvaraj, Yuvaraj, 1990, et al.
(författare)
-
Formal Development of Safe Automated Driving Using Differential Dynamic Logic
- 2023
-
Ingår i: IEEE Transactions on Intelligent Vehicles. - 2379-8858. ; 8:1, s. 988-1000
-
Tidskriftsartikel (refereegranskat)abstract
- The challenges in providing convincing arguments for safe and correct behavior of automated driving (AD) systems have so far hindered their widespread commercial deployment. Conventional development approaches such as testing and simulation are limited by non-exhaustive analysis, and can thus not guarantee safety in all possible scenarios. Formal methods can provide mathematical proofs that could be used to produce rigorous evidence to support the safety argument. This paper investigates the use of differential dynamic logic and the deductive verification tool KeYmaera X in the development of an AD feature. Specifically, this paper demonstrates how formal models and safety proofs of different design variants of a Decision & Control module can be used in the safety argument of an in-lane AD feature. In doing so, the assumptions and invariant conditions necessary to guarantee safety are identified, and the paper shows how such an analysis helps during the development process in requirement refinement and formulation of the operational design domain. Furthermore, it is shown how the performance of the different models is formally analyzed exhaustively, in all their allowed behaviors.
|
|
| 6. |
- 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.
|
|
| 7. |
- Selvaraj, Yuvaraj, 1990
(författare)
-
On Provably Correct Decision-Making for Automated Driving
- 2020
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- The introduction of driving automation in road vehicles can potentially reduce road traffic crashes and significantly improve road safety. Automation in road vehicles also brings several other benefits such as the possibility to provide independent mobility for people who cannot and/or should not drive. Many different hardware and software components (e.g. sensing, decision-making, actuation, and control) interact to solve the autonomous driving task. Correctness of such automated driving systems is crucial as incorrect behaviour may have catastrophic consequences. Autonomous vehicles operate in complex and dynamic environments, which requires decision-making and planning at different levels. The aim of such decision-making components in these systems is to make safe decisions at all times. The challenge of safety verification of these systems is crucial for the commercial deployment of full autonomy in vehicles. Testing for safety is expensive, impractical, and can never guarantee the absence of errors. In contrast, formal methods , which are techniques that use rigorous mathematical models to build hardware and software systems can provide a mathematical proof of the correctness of the system. The focus of this thesis is to address some of the challenges in the safety verification of decision-making in automated driving systems. A central question here is how to establish formal verification as an efficient tool for automated driving software development. A key finding is the need for an integrated formal approach to prove correctness and to provide a complete safety argument. This thesis provides insights into how three different formal verification approaches, namely supervisory control theory, model checking, and deductive verification differ in their application to automated driving and identifies the challenges associated with each method. It identifies the need for the introduction of more rigour in the requirement refinement process and presents one possible solution by using a formal model-based safety analysis approach. To address challenges in the manual modelling process, a possible solution by automatically learning formal models directly from code is proposed.
|
|
| 8. |
- 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.
|
|
| 9. |
- Selvaraj, Yuvaraj, 1990
(författare)
-
Safety Proofs for Automated Driving using Formal Methods
- 2022
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- The introduction of driving automation in road vehicles can potentially reduce road traffic crashes and significantly improve road safety. Automation in road vehicles also brings other benefits such as the possibility to provide independent mobility for people who cannot and/or should not drive. Correctness of such automated driving systems (ADSs) is crucial as incorrect behaviour may have catastrophic consequences. Automated vehicles operate in complex and dynamic environments, which requires decision-making and control at different levels. The aim of such decision-making is for the vehicle to be safe at all times. Verifying safety of these systems is crucial for the commercial deployment of full autonomy in vehicles. Testing for safety is expensive, impractical, and can never guarantee the absence of errors. In contrast, formal methods , techniques that use rigorous mathematical models to build hardware and software systems, can provide mathematical proofs of the correctness of the systems. The focus of this thesis is to address some of the challenges in the safety verification of decision and control systems for automated driving. A central question here is how to establish formal methods as an efficient approach to develop a safe ADS. A key finding is the need for an integrated formal approach to prove correctness of ADS. Several formal methods to model, specify, and verify ADS are evaluated. Insights into how the evaluated methods differ in various aspects and the challenges in the respective methods are discussed. To help developers and safety experts design safe ADSs, the thesis presents modelling guidelines and methods to identify and address subtle modelling errors that might inadvertently result in proving a faulty design to be safe. To address challenges in the manual modelling process, a systematic approach to automatically obtain formal models from ADS software is presented and validated by a proof of concept. Finally, a structured approach on how to use the different formal artifacts to provide evidence for the safety argument of an ADS is shown.
|
|
| 10. |
- Selvaraj, Yuvaraj, 1990, et al.
(författare)
-
Supervisory Control Theory in System Safety Analysis
- 2020
-
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. ; 12235, s. 9-22
-
Konferensbidrag (refereegranskat)abstract
- Development of safety critical systems requires a risk management strategy to identify and analyse hazards, and apply necessary actions to eliminate or control them as malfunctions could be catastrophic. Fault Tree Analysis (FTA) is one of the most widely used methods for safety analysis in industrial use. However, the standard FTA is manual, informal, and limited to static analysis of systems. In this paper, we present preliminary results from a model-based approach to address these limitations using Supervisory Control Theory. Taking an example from the Fault Tree Handbook, we present a systematic approach to incrementally obtain formal models from a fault tree and verify them in the tool Supremica. We present a method to calculate minimal cut sets using our approach. These compositional techniques could potentially be very beneficial in the safety analysis of highly complex safety critical systems, where several components interact to solve different tasks.
|
|
| 11. |
- Selvaraj, Yuvaraj, 1990, et al.
(författare)
-
Verification of Decision Making Software in an Autonomous Vehicle: An Industrial Case Study
- 2019
-
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. ; 11687 LNCS, s. 143-159
-
Konferensbidrag (refereegranskat)abstract
- Correctness of autonomous driving systems is crucial as incorrect behaviour may have catastrophic consequences. Many different hardware and software components (e.g. sensing, decision making, actuation, and control) interact to solve the autonomous driving task, leading to a level of complexity that brings new challenges for the formal verification community. Though formal verification has been used to prove correctness of software, there are significant challenges in transferring such techniques to an agile software development process and to ensure widespread industrial adoption. In the light of these challenges, the identification of appropriate formalisms, and consequently the right verification tools, has significant impact on addressing them. In this paper, we evaluate the application of different formal techniques from supervisory control theory, model checking, and deductive verification to verify existing decision and control software (in development) for an autonomous vehicle. We discuss how the verification objective differs with respect to the choice of formalism and the level of formality that can be applied. Insights from the case study show a need for multiple formal methods to prove correctness, the difficulty to capture the right level of abstraction to model and specify the formal properties for the verification objectives.
|
|
