Abstract
We present an approach to prove safety (collision freedom) of multi-lane motorway traffic with lane-change manoeuvres. This is ultimately a hybrid verification problem due to the continuous dynamics of the cars. We abstract from the dynamics by introducing a new spatial interval logic based on the view of each car. To guarantee safety, we present two variants of a lane-change controller, one with perfect knowledge of the safety envelopes of neighbouring cars and one which takes only the size of the neighbouring cars into account. Based on these controllers we provide a local safety proof for unboundedly many cars by showing that at any moment the reserved space of each car is disjoint from the reserved space of any other car.
This research was partially supported by the German Research Council (DFG) in the Transregional Collaborative Research Center SFB/TR 14 AVACS.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Lygeros, J., Godbole, D.N., Sastry, S.S.: Verified hybrid controllers for automated vehicles. IEEE Transactions on Automatic Control 43, 522–539 (1998)
Jula, H., Kosmatopoulos, E.B., Ioannou, P.A.: Collision avoidance analysis for lane changing and merging. Technical Report UCB-ITS-PRR-99-13, California Partners for Advanced Transit and Highways (PATH), Univ. of California at Berkeley (1999)
Werling, M., Gindele, T., Jagszent, D., Gröll, L.: A robust algorithm for handling traffic in urban scenarios. In: Proc. IEEE Intelligent Vehicles Symposium, Eindhoven, The Netherlands, pp. 168–173 (2008)
Damm, W., Hungar, H., Olderog, E.R.: Verification of cooperating traffic agents. International Journal of Control 79, 395–421 (2006)
Moor, T., Raisch, J., O’Young, S.: Discrete supervisory control of hybrid systems based on l-complete approximations. Discrete Event Dynamic Systems 12, 83–107 (2002)
Moor, T., Raisch, J., Davoren, J.: Admissiblity criteria for a hierarchical design of hybrid systems. In: Proc. IFAD Conf. on Analysis and Design of Hybrid Systems, St. Malo, France, pp. 389–394 (2003)
Habets, L.C.G.J.M., Collins, P., van Schuppen, J.: Reachability and control synthesis for piecewise-affine hybrid systems on simplices. IEEE Transactions on Automatic Control 51, 938–948 (2006)
Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. Computer 18, 10–19 (1985)
Zhou, C., Hoare, C., Ravn, A.: A calculus of durations. Information Processing Letters 40, 269–276 (1991)
Schäfer, A.: A Calculus for Shapes in Time and Space. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 463–477. Springer, Heidelberg (2005)
Woodcock, J., Davies, J.: Using Z – Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)
Alur, R., Dill, D.L.: A theory of timed automata. TCS 126, 183–235 (1994)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Hoare, C.A.R.: Communicating sequential processes. CACM 21, 666–677 (1978)
Hilscher, M., Linker, S., Olderog, E.R., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic maenoeuvres. Report 79, SFB/TR 14 AVACS (2011); ISSN: 1860-9821, avacs.org
Varaija, P.: Smart cars on smart roads: problems of control. IEEE Transactions on Automatic Control AC-38, 195–207 (1993)
Hsu, A., Eskafi, F., Sachs, S., Varaija, P.: Protocol design for an automated highway system. Discrete Event Dynamic Systems 2, 183–206 (1994)
Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. on Software Engineering 26, 687–701 (2000)
Faber, J., Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: Automatic Verification of Parametric Specifications with Complex Topologies. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 152–167. Springer, Heidelberg (2010)
van Benthem, J., Bezhanishvili, G.: Modal logics of space. In: Aiello, M., Pratt-Hartmann, I., Benthem, J. (eds.) Handbook of Spatial Logics, pp. 217–298. Springer, Heidelberg (2007)
Schäfer, A.: Axiomatisation and decidability of multi-dimensional duration calculus. Information and Computation 205, 25–64 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hilscher, M., Linker, S., Olderog, ER., Ravn, A.P. (2011). An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres. In: Qin, S., Qiu, Z. (eds) Formal Methods and Software Engineering. ICFEM 2011. Lecture Notes in Computer Science, vol 6991. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24559-6_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-24559-6_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24558-9
Online ISBN: 978-3-642-24559-6
eBook Packages: Computer ScienceComputer Science (R0)