https://www.mdu.se/

mdu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Towards a Two-layer Framework for Verifying Autonomous Vehicles
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-7663-5497
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-0904-3712
2019 (English)In: NASA Formal Methods. NFM 2019. Lecture Notes in Computer Science, vol 11460, 2019Conference paper, Published paper (Refereed)
Abstract [en]

Autonomous vehicles rely heavily on intelligent algorithms for path planning and collision avoidance, and their functionality and dependability could be ensured through formal verification. To facilitate the verification, it is beneficial to decouple the static high-level planning from the dynamic functions like collision avoidance. In this paper, we propose a conceptual two-layer framework for verifying autonomous vehicles, which consists of a static layer and a dynamic layer. We focus concretely on modeling and verifying the dynamic layer using hybrid automata and UPPAAL SMC, where a continuous movement of the vehicle as well as collision avoidance via a dipole flow field algorithm are considered. This framework achieves decoupling by separating the verification of the vehicle's autonomous path planning from that of the vehicle autonomous operation in a continuous dynamic environment. To simplify the modeling process, we propose a pattern-based design method, where patterns are expressed as hybrid automata. We demonstrate the applicability of the dynamic layer of our framework on an industrial prototype of an autonomous wheel loader.

Place, publisher, year, edition, pages
2019.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 11460
National Category
Engineering and Technology Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-43924DOI: 10.1007/978-3-030-20652-9_12ISI: 000657973800012Scopus ID: 2-s2.0-85066869584ISBN: 9783030206512 (print)OAI: oai:DiVA.org:mdh-43924DiVA, id: diva2:1327382
Conference
11th Annual NASA Formal Methods Symposium NFM 2019, 07 May 2019, Houston, United States
Projects
DPAC - Dependable Platforms for Autonomous systems and ControlAvailable from: 2019-06-19 Created: 2019-06-19 Last updated: 2022-04-22Bibliographically approved
In thesis
1. Automatic Model Generation and Scalable Verification for Autonomous Vehicles: Mission Planning and Collision Avoidance
Open this publication in new window or tab >>Automatic Model Generation and Scalable Verification for Autonomous Vehicles: Mission Planning and Collision Avoidance
2020 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Autonomous vehicles such as mobile driver-less construction equipment bear the promise of increased safety and industrial productivity by automating repetitive tasks and reducing manual labor costs. These systems are usually involved in safety- or mission-critical scenarios, therefore they require thorough analysis and verification. Traditional approaches such as simulation and prototype testing are limited in their scope of verifying a system that interacts autonomously with an unpredictable environment that assumes the presence of humans and varying site conditions. Methods for formal verification could be more suitable in providing guarantees of safe operation of autonomous vehicles within specified unpredictable environments. However, employing them entails addressing two main challenges: (i) constructing the models of the systems and their environment, and (ii) scaling the verification to the incurred model complexity. We address these two challenges for two essential aspects of autonomous vehicle design: mission planning and collision avoidance. Though inherently different, communication between these two aspects is necessary, as the information obtained from verifying collision avoidance can help to improve the mission planning and vice versa. Finding a solution that addresses both mission planning and collision avoidance modeling and verification, while decoupling them for solution maintainability is one crux of this study. Another one deals with demonstrating the applicability and scalability of the proposed approach on complex and industrial-level systems.

In this thesis, we propose a two-layer framework for mission planning and verification of autonomous vehicles. The framework separates the modeling and computing mission plans in a discrete environment, from the vehicle movement within a continuous environment, in which collision avoidance algorithms based on dipole fields are proven to ensure safe behavior. We call the layer for mission planning, the "static layer", and the other one the "dynamic layer". Due to the inherent difference between the layers, we use different modeling and verification approaches, namely: (i) the timed automata formalism and the UPPAAL model checker to compute mission plans for the autonomous vehicles, and (ii) hybrid automata and statistical model checking using UPPAAL Statistical Model Checker to verify collision avoidance and safe operation. We create model-generation algorithms, based on which we develop tool support for the static layer, called TAMAA (Timed-Automata-Based Planner for Autonomous Agents). The tool enables the designers to configure their systems and environments in a graphical user interface, and utilize formal methods and advanced path-planning algorithms to generate mission plans automatically. TAMAA also integrates reinforcement learning with model checking to alleviate the state-space explosion problem when the number of vehicles increases. We create a hybrid model for the dynamic layer of the framework and propose a pattern-based modeling method for the embedded control systems of the autonomous vehicles to ease the design and facilitate reuse. We validate the proposed framework and design method on an industrial use case involving autonomous wheel loaders, for which we verify invariance, reachability, and liveness properties.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2020
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 291
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-47918 (URN)978-91-7485-469-5 (ISBN)
Presentation
2020-06-15, Västerås Campus (+ Online/Zoom), Mälardalen University, Västerås, 09:00 (English)
Opponent
Supervisors
Projects
DPAC
Funder
Knowledge Foundation, 20150022
Available from: 2020-05-08 Created: 2020-05-07 Last updated: 2022-11-08Bibliographically approved
2. Formal Methods for Scalable Synthesis and Verification of Autonomous Systems: Mission Planning and Collision Avoidance
Open this publication in new window or tab >>Formal Methods for Scalable Synthesis and Verification of Autonomous Systems: Mission Planning and Collision Avoidance
2022 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Autonomous systems (a.k.a., agents) are often designed to move and execute tasks, without or with little human intervention. As the agents are often involved in safety- or mission-critical scenarios, ensuring the correctness of mission planning (i.e., path finding and task scheduling) and collision avoidance is crucial for such systems. However, traditional verification approaches, such as testing, are not sufficient to provide such assurance.

Formal methods such as model checking are well known for their rigorous verification based on mathematical models and logic rules, which provide guarantees of the absence of errors in system models. However, employing them entails tackling many challenges such as the complicated formal modeling and the scalability of the algorithmic methods. Additionally, the mission planning concerns the static and predictable factors in the working environment of the agents, such as stationary obstacles and predefined tasks, whereas the collision avoidance focuses on the dynamic and unpredictable factors, such as pedestrians. Consequently, certain questions arise in this context: (i) How can formal methods be applied in providing correctness-guaranteed solutions within a holistic framework that handles both the static mission planning and the dynamic collision avoidance?, and (ii)  When the methods for realizing the agents' artificial intelligence, such as machine learning, involve large amounts of data, how to improve the scalability of formal methods when verifying the results of such methods? In this dissertation, we offer answers to the questions by developing solutions in form of new frameworks and algorithms targeting the mentioned problems, implementing the solutions in software tools, and evaluating their performance on real-world applications.

We propose a two-layer framework for formal modeling and verification of agents. The framework separates the discrete mission planning from the continuous movement of agents, which is needed for collision avoidance verification. Additionally, different formal modeling and verification techniques are adopted in the two layers of the framework respectively.

For mission planning, we design two types of tool-supported approaches, one based on graphic search, and one based on learning. The former is sound and complete, and supported by the tools UPPAAL and UPPAAL TIGA. However, the graphic-search approach is not scalable for large numbers of agents. The learning-based solution complements the graphic-search one, by handling more agents, being supported by UPPAAL STRATEGO. As a trade-off, the learning-based method is sound but not complete. 

For the verification of collision avoidance, we propose two solutions, the first one based on statistical model checking in UPPAAL SMC, and the second one based on the symbolic model checking of UPPAAL STRATEGO. In the second solution, we transform the hybrid agent models, whose verification is undecidable, into a conservative over-approximation as a discrete-time model whose model checking is decidable. These results are proven as theorems in the dissertation.

To support our methods, we develop a toolset named MALTA that enables the automation of model construction and mission planning, and provides a visualization of environment configuration and the resulting mission plans. By using MALTA, we experiment with our novel methods in an industrial use case: an autonomous quarry. The experiment results demonstrate the advantages and weaknesses of different methods used in different types of environments, as well as the applicability of our methods and tool in complex systems.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2022
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 359
Keywords
autonomous agents, synthesis, verification, planning, collision avoidance, formal methods, model checking
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-58086 (URN)978-91-7485-552-4 (ISBN)
Public defence
2022-06-15, Gamma & online, Mälardalens universitet, Västerås, 13:00 (English)
Opponent
Supervisors
Projects
DPAC - Dependable Platforms for Autonomous systems and Control
Funder
Knowledge Foundation, 20150022
Available from: 2022-04-27 Created: 2022-04-22 Last updated: 2022-11-08Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Gu, RongMarinescu, RalucaSeceleanu, CristinaLundqvist, Kristina

Search in DiVA

By author/editor
Gu, RongMarinescu, RalucaSeceleanu, CristinaLundqvist, Kristina
By organisation
Embedded Systems
Engineering and TechnologyComputer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 202 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf