SPLAT! How to Avoid Bugs while Driving on the Highway

Download

Abstract

Abstract. A bug on your windshield does little damage, but a bug in the software that controls your engine, brakes or steering is catastrophic. Driver assistance technologies, like adaptive cruise control and automatic braking protocols, have the potential to increase the efficiency of crowded roads, but more compelling is their capacity for reducing the number of accidents and fatalities resulting from driver error. Yet, increased depen- dence on this next-generation technology is wise only when its reliability has been ensured and regulated.

Our methods can’t protect your windshield from insects as you cruise down the highway, but with continued research we can remove the dan- gerous software bugs in safety-critical systems that testing and model checking overlook.

References

  1. Ar ́echiga, N., Loos, S.M., Platzer, A., Krogh, B.H.: Using theorem provers to guar- antee closed-loop system properties. In: Tilbury, D. (ed.) ACC (2012)

  2. Loos, S.M., Platzer, A.: Safe intersections: At the crossing of hybrid systems and verification. In: Yi, K. (ed.) ITSC. pp. 1181–1186. Springer (2011)

  3. Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: Hybrid, distributed, and now formally verified. In: Butler, M., Schulte, W. (eds.) FM. LNCS, vol. 6664, pp. 42–56. Springer (2011)

  4. Mitsch, S., Loos, S.M., Platzer, A.: Towards formal verification of freeway traffic control. In: Lu, C. (ed.) ICCPS. pp. 171–180. IEEE (2012)

  5. Platzer, A.: Quantified differential dynamic logic for distributed hybrid systems. In: Dawar, A., Veith, H. (eds.) CSL. LNCS, vol. 6247, pp. 469–483. Springer (2010)

  6. Platzer, A.: Quantified differential invariants. In: Frazzoli, E., Grosu, R. (eds.)

    HSCC. pp. 63–72. ACM (2011)

  7. Platzer, A.: A complete axiomatization of quantified differential dynamic logic for

    distributed hybrid systems. Logical Methods in Computer Science (2012), special

    issue for selected papers from CSL’10

  8. Platzer, A.: Logics of dynamical systems. In: LICS. pp. 13–24. IEEE Computer

    Society (2012)

  9. Rajhans, A., Bhave, A., Loos, S.M., Krogh, B.H., Platzer, A., Garlan, D.: Using

    parameters in architectural views to support heterogeneous design and verification.

    In: CDC. pp. 2705–2710 (2011)

  10. Renshaw, D.W., Loos, S.M., Platzer, A.: Distributed theorem proving for dis-

    tributed hybrid systems. In: Qin, S., Qiu, Z. (eds.) ICFEM. LNCS, vol. 6991, pp. 356–371. Springer (2011)

Award ID: 0931985

 

  • 0931985
  • CPS Domains
  • Critical Infrastructure
  • SCADA Systems
  • Robotics
  • Transportation
  • Automotive
  • CPS Technologies
  • Embedded Software
  • Education
  • Foundations
  • Composition
  • Control
  • Modeling
  • Hybrid Models
  • Semantics
  • Validation and Verification
  • 2012
  • National CPS PI Meeting 2012
  • Poster
  • Academia
  • CPS PI MTG 12 Posters & Abstracts
Submitted by Andre Platzer on