tr-announce

Download

tr-announce@lists.rwth-aachen.de

April 2015

1 participants
2 discussions

2015-07: Experimental Validation and Mathematical Analysis of Cooperative Vehicles in a Platoon
by Thomas Ströder 15 Apr '15

15 Apr '15

The following technical report is available from http://aib.informatik.rwth-aachen.de: Experimental Validation and Mathematical Analysis of Cooperative Vehicles in a Platoon Hilal Diab AIB 2015-07 The infrastructure of roads in many countries is congested because of the rapid increase of the amount of traffic flow in the past few years. A significant part of this is due to the increase of freight transport, which is continuing to grow. Nowadays, safety on the roads and saving fuel should also be taken into consideration while finding the solutions to road congestion. One suggested solution to the problem is to increase the capacity of the highways. This can be realized by forming platoons of vehicles and automatically controlling the vehicles in order to maintain short, but at the same time, safe distances between the different vehicles within the platoon. The development of intelligent sensors and electronic control systems within vehicles make autonomous driving in platoons possible. Enabling vehicular wireless communication between the items of the platoon improves the performance of the controlled platoon significantly. Furthermore, enabling the platoon to communicate with other traffic members, such as other vehicles, intelligent traffic lights and infrastructure road units, allows the platoon to perform more complex driving scenarios for autonomous vehicles, such as crossing intersections. The first part of this thesis investigates the behavior of the platoon when only communication between its items is possible. The safety of the vehicles within the platoon is investigated, taking the effects of the communication faults on the behavior into account. This analysis could be helpful in the process of controller design, where the developed controller should ensure stability despite network failures and should achieve an optimal performance in every situation. Therefore, the verification of the controller behavior was investigated by formal verification methods: a reachability analysis of a dynamic and hybrid system. The safety of practical relevant scenarios was checked. In addition, a hardware platform was set up to test the platoon's behavior under the influence of hardware shortage, such as noises and time delays caused by hardware components. A 1:14 scaled platoon of four trucks equipped with sensors and WiFi modules was designed. This platform was used for testing different cooperative vehicle platoon controllers by examining their performance and influence on the safety in case of communication problems within the platoon. The second part of this thesis studies the behavior of the platoon when communication between the platoon and the intersection road unit is enabled. The following scenario has been considered: When a platoon of autonomous vehicles following a leader approaches an intersection, the platoon should change its highway mode to other modes in order to cross the intersection safely and efficiently. To realize that, information about the actual position of the platoon together with information of other vehicles in the intersection area are needed. Based on this information the platoon has to decide which mode should be performed. Therefore, we extended our platform with an indoor positioning system which is able to provide the position to the objects in a test environment independently. An intersection management system was implemented in order to test different scenarios related to different crossing modes of the platoon. Results showed that platoons can be controlled efficiently and safely while crossing the intersection.

1 0

2015-09: Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models
by Thomas Ströder 08 Apr '15

08 Apr '15

The following technical report is available from http://aib.informatik.rwth-aachen.de: Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models Xin Chen AIB 2015-09 With the ubiquitous use of computers in controlling physical systems, it requires to have a new formalism that could model both continuous flows and discrete jumps. Hybrid systems are introduced to this purpose. A hybrid system, which is modeled by a hybrid automaton in the thesis, is equipped with finitely many discrete modes and continuous real-valued variables. A state of it is then represented by a mode along with a valuation of the variables. Given that the system is in a mode l, the variable values are changed continuously according to the Ordinary Differential Equation (ODE) associated to l, or discretely by a jump starting from l. The thesis focuses on the techniques to compute all reachable states over a bounded time horizon and finitely many jumps for a hybrid system with non-linear dynamics. The results of that can then be used in safety verification of the system. Although a great amount of work has been devoted to the reachability analysis of hybrid systems with linear dynamics, there are few effective approaches proposed for the non-linear case which is very often in applications. The difficulty is twofold. Firstly, it is not easy to find an over-approximation with acceptable accuracy for a set of the solutions of a non-linear ODE. Secondly, to detect and compute the reachable states under a jump requires solving non-linear real arithmetic problems which is also difficult in general. In the thesis, we present our approaches to deal with the above difficulties. For the first one, we present the use of Taylor models as the over-approximate representations for non-linear ODE solutions. Our work can be viewed as a variant of the Taylor model method proposed by Berz et al., such that we are able to efficiently deal with some examples with more than $10$ variables. Besides, we also extend the work of Lin and Stadtherr to handle the ODEs with bounded time-varying parameters. For the second difficulty, we present two techniques: (a) domain contraction and (b) range over-approximation to compute an enclosure for the reachable set from which a jump is enabled. They can be seen as Satisfiability Modulo Theories (SMT) solving algorithms which are specialized for the reachability analysis of hybrid systems. In order to reduce the computational cost, we also propose different heuristics for aggregating Taylor models. Besides the above contributions, we describe a method to fast generate Taylor model over-approximations for linear ODE solutions. Its performance is demonstrated via a comparison with the tool SpaceEx. To make our methods accessible by other people, we implement them in a tool named Flow*. To examine the effectiveness, we thoroughly compare it with some related tools which are popularly used, according to their functionalities, over a set of non-trivial benchmarks that are collected by us from the areas of mechanics, biology, electronic engineering and medicine. From the experimental results, the advantage of Flow* over the other tools becomes more apparent when the scale of the system grows. On the other hand, it also shows that Flow* can be applied to analyzing realistic systems.

1 0