Mikael Asplund
Verifiable real-time coordination for safe cooperative drivingBackground and industrial relevanceAs the number of road vehicles in the world crosses the 1 billion mark and the future travel needs of the world population keep increasing, we are also paying an increasingly heavy price. Every year nearly 1.2 million people get killed in traffic, and as many die from urban pollution. Moreover, transportation stands for 23% of the total emissions of carbon dioxide in the European Union. Better software allows us to make transportation smarter, safer, and more efficient, thereby ameliorating some of the adverse effects of road-based transport. Modern vehicles are equipped with a wide range of sensors and driver assistance systems and there are already a number of self-driving cars that are being tested by the major automotive companies. The next big challenge is to enable efficient coordination among smart vehicles to further increase the safety and efficiency of the traffic. Significant real-world steps towards this goal have been taken, for example the Grand Cooperative Driving Challenge, the Sartre project, and the DRIVE C2X project. Moreover, standardisation efforts have come a long way with regards to low level communication, security mechanisms, and applications such as position information and warning messages. For heavy-duty vehicles, the ability to drive in platoons can present significant fuel-savings which makes it an economically very attractive technology. Both Scania and Volvo are developing platooning technology solutions towards this end. Obviously, there are strict safety requirements that must be upheld in these systems. Currently, these safety policies are a matter for the automotive companies to setup and agree upon. However, as these system become more prevalent and the impact of a potential failure increases, we can expect higher demands on safety-assurance in terms of testing and rigorous software development processes. This will hold the manufacturers accountable for the safety of their products. This project focuses on how to achieve reliable coordination mechanisms between vehicles which can be formally shown to fulfil a given specification. Such mechanisms would be of great importance when designing application level components, since this will reduce the number of special cases (e.g., a communication failure during a critical phase) which would otherwise have to be dealt with by the application designers. This has the potential to significantly reduce development costs (finding faults early), and to increase the reliability of the end products. Project descriptionWe found this project on three pillars: the current state of the art in vehicular real-time communication and safety message dissemination, new advances in formal methods allowing previously intractable problems to be solved, and the mature body of work concerning fault-tolerant algorithms for distributed systems. Platooning for heavy-duty vehicles will serve as the main application area and demonstration platform with Scania AB acting as a key reference. The project will iterate on the following three objectives.
In order to enable rigorous development methods for vehicle coordination, it is imperative to have a clear and unambiguous modelling language. Currently, the descriptions of vehicle behaviour is either done using semi-formal natural language specifications in industry standardisation efforts (e.g., ETSI standards), or using formal but very restricted mathematical notation (e.g., quantified differential dynamic logic) which can be unpractical to use in industrial development projects. In this project we aim to strike a balance by developing a modelling language which is both expressive enough to be used to describe vehicle behaviour and that lends itself to formal reasoning allowing the described behaviour to be formally proven correct.  Figure 1, Architecture Designing distributed algorithms which can be ensured to perform correctly also under faulty conditions is widely recognised as a hard problem. However, over the last few decades researchers have found a number of very useful abstraction and basic mechanisms (e.g., failure detectors, membership service, reliable broadcast primitives) which allows building fault-tolerant applications without having to solve the fault tolerance aspects from scratch every time. Vehicular coordination presents a new set of challenges due to the increased mobility and the dynamism of the number of participants so classical concepts like consensus cannot be easily implemented. However, we make use of recent advances in real-time communication and group membership research for vehicular systems to design robust and secure communication and coordination primitives. Figure 1 shows a possible architecture for a system where cooperative safety-critical applications can be designed with the support of a number of reliability services. On top of the basic services such as local vehicle information (e.g., vehicle speed), environmental sensors (e.g., radar) and basic communication, we will aim to create a set of fault-tolerant services which can guarantee properties such as timely message delivery. With the help of these, it is then possible to create high-level services such as reliable geocast. An important aspect of designing a reliable service is the ability to formally prove its correctness under a given fault model. However, proving properties about hybrid systems where continuous and discrete control interact (as is the case for vehicular coordination problems) is a long-standing research problem. Moreover, in the case of vehicular communication, one needs also to prove correctness of timed communication protocols (which until recently could not be done with more than a handful of nodes). Our approach to formally verify vehicular coordination algorithms is based on satisfiability modulo theories (SMT) reasoning. VisionThe overreaching ambition of this project is to advance the knowledge on how to develop reliable collaborative transportation systems. By combining formal verification principles and classical methods for distributed algorithms with novel coordination protocols, we believe that we can contribute to the development of better, smarter and safer software. By providing a set of useful coordination mechanisms together with proof strategies which allow these coordination mechanisms to be proven to be correct, we aim to enable a new direction of research which focus on fault-tolerant coordination algorithms for vehicular systems. The principal investigator (PI) is Mikael Asplund who works an assistant professor in the Real-time Systems Laboratory (RTSLAB), Department of Computer and Information Science, at Linköping University. Research environment and industrial cooperationThe Real-time Systems Laboratory conducts research on dependability and resource management in distributed systems. The PI also maintains collaboration with the distributed systems group in Trinity College Dublin where he worked as a Research Fellow with research problems related to vehicular computing. Scania is a major manufacturer of trucks and busses with headquarters in Södertälje, Sweden. Scania has a long history of innovation including pioneering the use of alternative fuels and fuel-efficient vehicles. Today, Scania is one of the leading actors in the development of vehicle platoons where trucks can drive in caravans with a shorter distance than possible with purely human driving. The aim of this project is to work on problems which are relevant for Scania (e.g., secure membership protocols for platoons) as well as to continuously share and present results to Scania to get feedback on the real-world relevance and issues. Publications
|
|
 |