Abstract
In this paper, we present a general methodology to estimate safety related parameter values of cooperative cyber-physical system-of-systems. As a case study, we consider a vehicle platoon model equipped with a novel distributed protocol for coordinated emergency braking. The estimation methodology is based on learning-based testing; which is an approach to automated requirements testing that combines machine learning with model checking.
Our methodology takes into account vehicle dynamics, control algorithm design, inter-vehicle communication protocols and environmental factors such as message packet loss rates. Empirical measurements from road testing of vehicle-to-vehicle communication in a platoon are modeled and used in our case study. We demonstrate that the minimum global time headway for our platoon model equipped with the CEBP function scales well with respect to platoon size.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
See www.safecop.eu.
- 2.
The measurements were done while the first author was employed at RISE − The Swedish Research Institute (previously SP − Technical Research Institute of Sweden).
- 3.
Recall that propositional LTL extends basic propositional logic with the temporal modalities G(\(\phi \)) (always \(\phi \)), F(\(\phi \)) (sometime \(\phi \)) and X(\(\phi \)) (next \(\phi \)). Other derived operators and past operators may also be included. See e.g. [12] for details.
- 4.
Infinite counter-examples to LTL liveness formulas are truncated around the loop, and the weaker test verdict warning may be issued.
- 5.
Assuming \(V_{i+1}\) maintains its speed at time t.
- 6.
Clearly \(HW_{min}\) is a function of the many individual parameters of each vehicle \(V_i\) such as its weight, braking power etc. Different values of \(HW_{min}\) will thus be obtained if individual vehicle parameters are changed. For simplicity, we have assumed a homogeneous platoon, i.e. all vehicle parameters are the same. .
- 7.
It is also possible to use SUT observations between the output cycles by thresholding. This can yield greater accuracy, but this approach was not taken here.
- 8.
These terminating neutral commands 0 were redundant by the design of CEBP, but extended the test case until the platoon was stopped.
References
Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)
Bennaceur, A., Meinke, K.: Machine learning for software analysis: models, methods, and applications. In: Bennaceur, A., Hähnle, R., Meinke, K. (eds.) Machine Learning for Dynamic Software Analysis: Potentials and Limits. LNCS, vol. 11026, pp. 3–49. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96562-8_1
Bergenhem, C., Shladover, S., Coelingh, E., Englund, C., Shladover, S., Tsugawa, S.: Overview of platooning systems. In: Proceedings of 19th ITS World Congress, Vienna, Austria, October 2012
van den Bleek, R.: Design of a hybrid adaptive cruise control stop-&-go system. Master’s thesis, Technische Universiteit Eindhoven, Department of Mechanical Engineering (2007)
Bohm, A., Jonsson, M., Kunert, K., Vinel, A.: Context-aware retransmission scheme for increased reliability in platooning applications. In: Sikora A., Berbineau M., Vinel A., Jonsson M., Pirovano A., Aguado M. (eds.) Communication Technologies for Vehicles. Nets4Cars/Nets4Trains/Nets4Aircraft 2014. LNCS, vol. 8435, pp. 30–42. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06644-8_4
Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_29
Colin, S., Lanoix, A., Kouchnarenko, O., Souquieres, J.: Using CSPIIb components: application to a platoon of vehicles, pp. 103–118. Springer, Heidelberg (2009)
Dolk, V.S., Ploeg, J., Heemels, M.: Event-triggered control for string-stable vehicle platooning. IEEE Trans. Intell. Transp. Syst. 18(12), 3486–3500 (2017)
El-Zaher, M., Contet, J., Gruer, P., Gechter, F., Koukam, A.: Compositional verification for reactive multi-agent systems applied to platoon non collision verification. Stud. Inform. Univ. 10(3), 119–141 (2012)
European Telecommunications Standards Institute: Intelligent Transport Systems (ITS); Access layer specification for Intelligent Transport Systems operating in the 5 GHz frequency band. EN 302 663 V1.2.1, ETSI, July 2013
Feng, L., Lundmark, S., Meinke, K., Niu, F., Sindhu, M.A., Wong, P.Y.H.: Case studies in learning-based testing. In: YenigĂ¼n, H., Yilmaz, C., Ulrich, A. (eds.) ICTSS 2013. LNCS, vol. 8254, pp. 164–179. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41707-8_11
Fisher, M.: An Introduction to Practical Formal Methods Using Temporal Logic. Wiley Publishing, Chichester (2011)
Giordano, G., Segata, M., Blanchini, F., Cigno, R.L.: A joint network/control design for cooperative automatic driving. In: 2017 IEEE Vehicular Networking Conference (VNC), pp. 167–174, November 2017
De la Higuera, C.: Grammatical Inference: Learning Automata and Grammars. Cambridge University Press, Cambridge (2010)
IPG Automotive: Brochure about CarMaker, TruckMaker and MotorcycleMaker (2018). https://ipg-automotive.com/pressmedia/media-library/. Accessed 11 June 2018
Kakade, R.S.: Automatic Cruise control system. Master’s thesis, Indian Institute of Technology, Department of Systems and Control Engineering, Mumbai (2007)
Kamali, M., Dennis, L.A., McAree, O., Fisher, M., Veres, S.M.: Formal verification of autonomous vehicle platooning. Sci. Comput. Programm. 148, 88–106 (2017)
Karlsson, K., Carlsson, J., Larsson, M., Bergenhem, C.: Evaluation of the V2V channel and diversity potential for platooning trucks. In: Antennas and Propagation (EuCAP) Proceedings of the 10th European Conference, Davos, Switzerland, 11–15 April 2016 (2016)
Khosrowjerdi, H., Meinke, K.: Learning-based testing for autonomous systems using spatial and temporal requirements. In: Proceedings of 1st International Workshop on Machine Learning and Software Engineering in Symbiosis. IEEE (2018)
Liang, K.Y., MĂ¥rtensson, J., Johansson, K.H.: Heavy-duty vehicle platoon formation for fuel efficiency. IEEE Trans. Intell. Transp. Syst. 17(4), 1051–1061 (2016)
Meinke, K., Sindhu, M.A.: Incremental learning-based testing for reactive systems. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 134–151. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21768-5_11
Meinke, K.: Learning-based testing of cyber-physical systems-of-systems: a platooning study. In: Reinecke, P., Di Marco, A. (eds.) EPEW 2017. LNCS, vol. 10497, pp. 135–151. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66583-2_9
Meinke, K., Sindhu, M.A.: LBTest: a learning-based testing tool for reactive systems. In: Proceedings of the 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation, ICST 2013, pp. 447–454. IEEE Computer Society (2013)
Murthy, D.K., Masrur, A.: Braking in close following platoons: the law of the weakest. In: 2016 Euromicro Conference on Digital System Design (DSD), pp. 613–620, August 2016
Oncu, S., Van de Wouw, N., Heemels, M., Nijmeijer, H.: String stability of interconnected vehicles under communication constraints. In: 2012 IEEE 51st Annual Conference on Decision and Control (CDC), pp. 2459–2464. IEEE (2012)
Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Formal Methods for Protocol Engineering and Distributed Systems. IAICT, vol. 28, pp. 225–240. Springer, Boston, MA (1999). https://doi.org/10.1007/978-0-387-35578-8_13
Swaroop, D., Hedrick, J.: String stability of interconnected systems. IEEE Trans. Autom. Control 41, 349–357 (1996)
Trochez, D., Tsakalos, A.: Adaptive cruise control implementation with constant range and constant time-gap policies. Master’s thesis, KTH Royal Institute of Technology, EECS School (2017)
Valiant, L.G.: A theory of the learnable. Commun. ACM 27(11), 1134–1142 (1984)
Vinel, A., Lyamin, N., Isachenkov, P.: Modeling of V2V communications for C-ITS safety applications: a CPS perspective. IEEE Commun. Lett. PP(99), 1 (2018)
van Willigen, W.H., Schut, M.C., Kester, L.J.H.M.: Evaluating adaptive cruise control strategies in worst-case scenarios. In: 2011 14th International IEEE Conference on Intelligent Transportation Systems (ITSC), pp. 1910–1915, October 2011
Willke, T.L., Tientrakool, P., Maxemchuk, N.F.: A survey of inter-vehicle communication protocols and their applications. Commun. Surveys Tuts. 11(2), 3–20 (2009). https://doi.org/10.1109/SURV.2009.090202
Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. STTT 8(3), 216–228 (2006)
Acknowledgement
The research leading to these results has been performed in the SafeCOP project, that received funding from the ECSEL Joint Undertaking under grant agreement 692529, and from Vinnova Swedish national funding. The work was partially performed in the Next Generation Electrical Architecture (NGEA) step2 project, funded by the Vinnova FFI-programme. We express special thanks for valuable comments to Magnus Jonsson and Alexey Vinel of Halmstad University.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Bergenhem, C., Meinke, K., Ström, F. (2018). Quantitative Safety Analysis of a Coordinated Emergency Brake Protocol for Vehicle Platoons. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems. ISoLA 2018. Lecture Notes in Computer Science(), vol 11246. Springer, Cham. https://doi.org/10.1007/978-3-030-03424-5_26
Download citation
DOI: https://doi.org/10.1007/978-3-030-03424-5_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03423-8
Online ISBN: 978-3-030-03424-5
eBook Packages: Computer ScienceComputer Science (R0)