Formal Model Validation by Reachset Conformance between Low and High Order Tractor Semitrailer Vehicle Models

Abstract

The blooming era of vehicle automation is shaping the future of transportation in ways that humans were not expecting a few decades ago. Autonomous vehicles rely on vehicle models to plan their trajectories and their control behaviour. In this thesis work, a formal model validation technique is presented to check for the validity of the dynamics of low order models against higher order models or even against real measurable systems. The aim is to determine the required bounds of unstructured uncertainties for model validation. First, a formal approach for modelling of the dynamics of vehicles with an arbitrary number of units is introduced which makes use of the Taylor series expansion. Next, the model validation procedure is carried out using reachset conformance falsification, where the dynamics of a high order model are explored using rapidly exploring random trees, and checked against reachable sets calculated for the linear low order model with uncertainties. While the method applied for quantifying the unstructured uncertainty between the low and high order models is based on a proportionality approach, it is also proposed that the higher order terms from the Taylor series could be a good candidate for the quantifying of the uncertainties. The methods presented are applied to a tractor semitrailer model and tested upon a suite of lane change maneuvers of different aggressiveness. The outcome is that the models conform in conservative maneuvers but fail to conform in aggressive maneuvers unless more unstructured uncertainty is introduced to the low order model. The effect of increasing the uncertainties on the robustness and performance of the studied models is also touched upon in the presented work.