Provably-Correct Compositional Synthesis of Vehicle Safety Systems

  • Petter Nilsson
  • Necmiye OzayEmail author
Part of the Unmanned System Technologies book series (UST)


As the automobile evolves toward full autonomy, many driver convenience and safety automation systems are being introduced into production vehicles. These systems often include controllers designed for individual tasks. Designing individual controllers for interacting subsystems, and composing them in a way that preserves the guarantees that each controller provides on each subsystem, is a challenging task. This chapter presents recent results addressing this problem through the use of formal methods and correct-by-construction controller synthesis. Mechanisms for handling implementation- and model imperfections, and contract-based composition of functionality, are discussed. The ideas are demonstrated in high-fidelity simulations in CarSim, and also on a real vehicle in Mcity, the autonomous vehicle testing facility at the University of Michigan.



The authors would like to thank Kwesi Rutledge for help with CarSim simulations and the Mcity implementation, Jessy Grizzle for useful discussions on vehicle safety systems, Stanley Smith for his contributions at the early stages of the work, and the Mcity team for assistance with experiments. This work is supported in part by NSF grants CNS-1239037, CNS-1446298, and ECCS-1553873, and by Toyota Research Institute (TRI). TRI provided funds to assist the authors with their research, but this chapter solely reflects the opinions and conclusions of the authors and not those of TRI or any other Toyota entity.


  1. 1.
    G. Frehse, Z. Han, B. Krogh, Assume-guarantee reasoning for hybrid i/o-automata by over-approximation of continuous interaction, in Proceedings of IEEE CDC (2004), pp. 479–484Google Scholar
  2. 2.
    L. Benvenuti, A. Ferrari, E. Mazzi, A.L. Sangiovanni-Vincentelli, Contract-based design for computation and verification of a closed-loop hybrid system, in Proceedings of HSCC (2008), pp. 58–71Google Scholar
  3. 3.
    P. Nuzzo, H. Xu, N. Ozay, J.B. Finn, A.L Sangiovanni-Vincentelli, R.M. Murray, A. Donzé, S.A Seshia, A contract-based methodology for aircraft electric power system design. IEEE Access 2, 1–25 (2014)CrossRefGoogle Scholar
  4. 4.
    I. Filippidis, Decomposing formal specifications into assume-guarantee contracts for hierarchical system design. Ph.D. thesis, California Institute of Technology, 2018Google Scholar
  5. 5.
    E.S. Kim, M. Arcak, S.A. Seshia, Compositional controller synthesis for vehicular traffic networks, in Proceedings of IEEE CDC (2015), pp. 6165–6171Google Scholar
  6. 6.
    P. Nilsson, N. Ozay, Synthesis of separable controlled invariant sets for modular local control design, in Proceedings of ACC (2016), pp. 5656–5663Google Scholar
  7. 7.
    S. Smith, P. Nilsson, N. Ozay, Interdependence quantification for compositional control synthesis: an application in vehicle safety systems, in Proceedings of IEEE CDC (2016), pp. 5700 – 5707Google Scholar
  8. 8.
    F. Blanchini, Set invariance in control. Automatica 35(11), 1747–1767 (1999)MathSciNetCrossRefGoogle Scholar
  9. 9.
    E. De Santis, M.D. Di Benedetto, L. Berardi, Computation of maximal safe sets for switching systems. IEEE Trans. Autom. Control 49(2), 184–195 (2004)MathSciNetCrossRefGoogle Scholar
  10. 10.
    P. Nilsson, O. Hussien, A. Balkan, Y. Chen, A. Ames, J. Grizzle, N. Ozay, H. Peng, P. Tabuada, Correct-by-construction adaptive cruise control: two approaches. IEEE Trans. Control Syst. Technol. 24(4), 1294–1307 (2016)CrossRefGoogle Scholar
  11. 11.
    E.J. Rossetter, J. Christian Gerdes, Lyapunov based performance guarantees for the potential field lane-keeping assistance system. J. Dyn. Syst. Meas. Control. 128(3), 510–522 (2006)CrossRefGoogle Scholar
  12. 12.
    G.J.L. Naus, J. Ploeg, M.J.G. Van de Molengraft, W.P.M.H. Heemels, M. Steinbuch, Design and implementation of parameterized adaptive cruise control: an explicit model predictive control approach. Control. Eng. Pract. 18(8), 882–892 (2010)CrossRefGoogle Scholar
  13. 13.
    S. Ishida, J.E. Gayko, Development, evaluation and introduction of a lane keeping assistance system, in IEEE Intelligent Vehicles Symposium (2004), pp. 943–944Google Scholar
  14. 14.
    D. Hoehener, G. Huang, D. Del Vecchio, Design of a lane departure driver-assist system under safety specifications, in Proceedings of IEEE CDC (2016), pp. 2468–2474Google Scholar
  15. 15.
    T. Korssen, V. Dolk, J. van de Mortel-Fronczak, M. Reniers, M. Heemels, Systematic model-based design and implementation of supervisors for advanced driver assistance systems. IEEE Trans. Intell. Transp. Systems PP, 1–12 (2017)Google Scholar
  16. 16.
    K. Chatterjee, T.A. Henzinger, Assume-Guarantee Synthesis, in Proceedings of TACAS (2007), pp. 261–275Google Scholar
  17. 17.
    L. Benvenuti, A. Ferrari, E. Mazzi, A.L. Sangiovanni-Vincentelli, Contract-based design for computation and verification of a closed-loop hybrid system, in Proceedings of HSCC, ed. by M. Egerstedt, B. Mishra (2008), pp. 58–71Google Scholar
  18. 18.
    X. Xu, J.W. Grizzle, P. Tabuada, A.D. Ames, Correctness guarantees for the composition of lane keeping and adaptive cruise control. IEEE Trans. Autom. Sci. Eng. PP(99), 1–14 (2017)Google Scholar
  19. 19.
    M. Korda, D. Henrion, C.N. Jones, Convex computation of the maximum controlled invariant set for polynomial control systems. SIAM J. Control Optim. 52(5), 2944–2969 (2014)MathSciNetCrossRefGoogle Scholar
  20. 20.
    P. Tabuada, Verification and Control of Hybrid Systems: A Symbolic Approach (Springer Science & Business Media, New York, 2009)CrossRefGoogle Scholar
  21. 21.
    A.D. Ames, X. Xu, J.W. Grizzle, P. Tabuada, Control barrier function based quadratic programs for safety critical systems. IEEE Trans. Autom. Control. 62(8), 3861–3876 (2017)MathSciNetCrossRefGoogle Scholar
  22. 22.
    E.S. Kim, M. Arcak, S.A. Seshia, A small gain theorem for parametric assume-guarantee contracts, in Proceedings of HSCC (ACM, New York, 2017), pp. 207–216zbMATHGoogle Scholar
  23. 23.
    D.P. Bertsekas, Infinite time reachability of state-space regions by using feedback control. IEEE Trans. Autom. Control 17(5), 604–613 (1972)MathSciNetCrossRefGoogle Scholar
  24. 24.
    E.G. Gilbert, K. Tin Tan, Linear systems with state and control constraints: the theory and application of maximal output admissible sets. IEEE Trans. Autom. Control 36(9), 1008–1020 (1991)MathSciNetCrossRefGoogle Scholar
  25. 25.
    M. Rungger, P. Tabuada, Computing robust controlled invariant sets of linear systems. IEEE Trans. Autom. Control 62(7), 3665–3670 (2017)MathSciNetCrossRefGoogle Scholar
  26. 26.
    M. Herceg, M. Kvasnica, C.N. Jones, M. Morari, Multi-parametric toolbox 3.0, in Proceedings of the European Control Conference (2013), pp. 502–510Google Scholar
  27. 27.
    P. Nilsson, Correct-by-construction control synthesis for high-dimensional systems. Ph.D. thesis, University of Michigan, 2017Google Scholar
  28. 28.
    J. Liu, N. Ozay, Finite abstractions with robustness margins for temporal logic-based control synthesis. Nonlinear Anal. Hybrid Syst. 22, 1–15 (2016)MathSciNetCrossRefGoogle Scholar
  29. 29.
    CarSim (Mechanical Simulation).
  30. 30.

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.California Institute of TechnologyPasadenaUSA
  2. 2.University of MichiganAnn ArborUSA

Personalised recommendations