Safety Assessment of Networked Vehicle Platoon Controllers – Practical Experiences With Available Tools

Vehicle platoons are usually modelled as continuous dynamic systems. But the parameters of the embedded controllers require particular adaptation depending on the quality and changes commonly occurring in communication networks. These changes may lead to delays or in extreme cases to loss of information. Hence, these changes trigger the jump from one continuous state to another and may be considered as discrete events arising, in general, spontaneously. In this work, we use the formalism of hybrid automata to carry out a safety analysis of controlled vehicle platoons. We are interested in the safety verification of a platoon of vehicles, which communicate with each other via a wireless network. Our aim is to check, if a collision could take place within the platoon under a predefined control law including mode switches. In this paper, we report on results for the non-switching case and for pre-defined switching times. In addition, using different verification tools for this case study allows for the assessment of the performance of these tools and their limitations.