Application of Abstract Interpretation to the Automotive Electronic Control System

  • Tomoya YamaguchiEmail author
  • Martin Brain
  • Chirs Ryder
  • Yosikazu Imai
  • Yoshiumi Kawamura
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11388)


The verification and validation of industrial automotive systems is increasingly challenging as they become larger and more complex. Recent automotive Electric Control Units (ECUs) have approximately one half to one million of lines of code, and a modern automobile can contain hundreds of controllers. Significant work-hours are needed to understand and manage systems of this level of complexity. One particular challenge is understanding the changes to the software across development phases and revisions. To this end, we present a code dependency analysis tool that enhances designer understanding. It combines abstract interpretation and graph based data analysis to generate visualized dependency graphs on demand to support designer’s understanding of the code. We demonstrate its value by presenting dependency graph visuals for an industrial application, and report results showing significant reduction of work-hours and enhancement of the ability to understand the software.


  1. 1.
    Haughey, B.: Design Review Based on Failure Modes (DRBFM) and Design Review Based on Test Results (DRBTR) Process Guidebook. SAE International, Warrendale (2012)CrossRefGoogle Scholar
  2. 2.
    Cytron, R., et al.: An efficient method of computing static single assignment form. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 25–35. ACM (1989)Google Scholar
  3. 3.
    Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference on Software Engineering. IEEE Press (1981)Google Scholar
  4. 4.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM (1977)Google Scholar
  5. 5.
    D’Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 27(7), 1165–1178 (2008)CrossRefGoogle Scholar
  6. 6.
    Aho, A.V.: Compilers: Principles, Techniques and Tools (for Anna University), 2/e. Pearson Education India, Bengaluru (2003)Google Scholar
  7. 7.
  8. 8.
  9. 9.
    Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). Scholar
  10. 10.
  11. 11.
    Tesoriero, C.: Getting Started with OrientDB. Packt Publishing Ltd., Birmingham (2013)Google Scholar
  12. 12.
  13. 13.
  14. 14.
    Blazy, S., Bühler, D., Yakobowski, B.: Structuring abstract interpreters through state and value abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 112–130. Springer, Cham (2017). Scholar
  15. 15.
    Blanchet, B., et al.: A static analyzer for large safety-critical software. In: PLDI 2003, pp. 196–207 (2003)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Tomoya Yamaguchi
    • 1
    Email author
  • Martin Brain
    • 2
  • Chirs Ryder
    • 3
  • Yosikazu Imai
    • 4
  • Yoshiumi Kawamura
    • 1
  1. 1.Toyota Motor CorporationSusonoJapan
  2. 2.University of OxfordOxfordUK
  3. 3.DiffblueOxfordUK
  4. 4.Nu-softKouhoku, YokohamaJapan

Personalised recommendations