You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at http://www.ieee.org/web/publications/rights/copyrightpolicy.html)
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at http://www.acm.org/pubs/copyright_policy/)
  • technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact webmaster@ide.mdh.se

Automatic Model Generation and Scalable Verification for Autonomous Vehicles

Authors:


Publication Type:

Licentiate Thesis

ISRN:

978-91-7485-469-5


Abstract

Autonomous vehicles such as mobile driverless 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.

Bibtex

@misc{Gu5836,
author = {Rong Gu},
title = {Automatic Model Generation and Scalable Verification for Autonomous Vehicles},
month = {June},
year = {2020},
url = {http://www.es.mdh.se/publications/5836-}
}