Verification of Automotive Control Units

  • Tom Bienmüllor
  • Jürgon Bohn
  • Henning Brinkmann
  • Udo Brockmeyer
  • Werner Damm
  • Hardi Hungar
  • Peter Jansen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1710)


This paper describes the application of model-checking based verification tools to specification models of automotive control units. It firstly discusses the current state of a tool set which copes with discrete controllers described in STATEMATE, and then reports on proposed extensions currently under development to deal with hybrid ones which involve continuous values, too. First results based on an extension of abstraction techniques to verify such units are reported.


Verification Tool Discrete Controller Abstraction Technique Diagnosis Verification Verification Optimization 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. BBD+99.
    Torn Bienmüller, Udo Brockmeyer, Werner Damm, Gert Döhmen, Claus Eβmann, Hans-Jürgen Holberg, Hardi Hungar, Bernhard Josko, Rainer Schlör, Gunnar Wittich, Hartmut Wittke, Geoffrey Clements, John Rowlands, and Eric Sefton. Formal Verification of au Avionics Application using Abstraction and Symbolic Model Checking. In Felix Redmill and Tom Anderson, editors, Towards System Safety Proccedings of the Seventh SafetY-Proceedings of the Seventh Safety-Critical Systems Symposium. Huntingdon. UK, pages 150–173. Safety-Critical Systems Club, Springer Verlag, 1999.Google Scholar
  2. BBLS92.
    S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property preserving simulations. In G.v. Bachmann and D.K. Probst, editors, 4th Int. Workshop on Computer Aided Verification, LNCS 663, pages 260–273. Springer, 1992.Google Scholar
  3. BDG+98.
    J. Bohn, W. Damm, O. Grumberg, H. Hungar, and K. Laster. First-order CTL model checking. In V. Arvind and R. Ramanujam, editors, FSTTCS 98, LNCS 1530, pages 283–294, 1998.Google Scholar
  4. Bri99.
    Henning Brinkmann. Verifikation eines hybriden Steuersystems mit Hilfe erweiterter Abstraktiosmethoen. Master's thesis, Carl von Ossietzky Universitat Oldenburg, February 1999.Google Scholar
  5. Bry92.
    Randal B. Bryant. Symbolic boolean Manipulation with ordered Binary-Decision Diagrams. ACM Comp. Surveys. 24:293–318, 1992.CrossRefGoogle Scholar
  6. CES83.
    Edmund M. Clarke, B.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In Proccedings of the 10th ACM Symposium on Principles of Programming Languages, pages 117–126, 1983.Google Scholar
  7. CGL94.
    Edmund M. Clarke, Oma Grumberg, and David B. Long. Model checking and abstraction. In ACM Transactions on Programming Languages and Systems, volume 1G, pages 1512–1542, September 1994.CrossRefGoogle Scholar
  8. DJHP98.
    Werner Damm, Bernhard Jeske, Hardi Hungar, and Amir Pnueli. A compositional real-time semantics of STATEMATE designs. In W.-P. de Roever, editor, Proceedings. International Symposium on Compositionality The Significant Difference, LNCS 153G, pages 186–238. Springer-Verlag, 1998.CrossRefGoogle Scholar
  9. DJS95.
    W. Damm, B. Jeske, and R. Schöldr. Specification and verification of VHDL-based system-level hardware designs. In E. Börger, editor, SpeCification and Validition Methods, pages 331–410. Oxford Univ. Press, 1995.Google Scholar
  10. HGD95.
    H. Hungar, O. Grumberg, and W. Damm. what if model checking must be truly symbolic. In P. Camurati and H. Eveking, editors, CHARME 95, LNCS 987, pages 120. Springer Verlag, 1995.Google Scholar
  11. HHWT97.
    T.A. Henzinger, P.-H. He, and H. Wong-Toi. HyTech: A model checker for hybrid systems. SoftwaTe Tools fOT Technology Transfer, 1:110–122, 1997.zbMATHCrossRefGoogle Scholar
  12. Hoa69.
    C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576–583, 1969.zbMATHCrossRefGoogle Scholar
  13. Jos93.
    Bernhard Josk0. Modular Specification and Verification of Reactive terms. Carl von Ossietzky Universitat Oldenburg, 1993. Habiltaticnsschrift.Google Scholar
  14. Kur97.
    R.P. Kurshan. Formal verification in a commercial setting. In Proc. 84th Design Automation Conference, pages 258–262, 1997.Google Scholar
  15. McM93.
    Kenneth L. Mckdillan. Symbohc Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
  16. WoI8G.
    Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic. In Procecdinqs of the 18th Annual ACAf Symposium in Principles of Programmking Languages, pages 184–193, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Tom Bienmüllor
    • 1
  • Jürgon Bohn
    • 2
  • Henning Brinkmann
    • 1
  • Udo Brockmeyer
    • 2
  • Werner Damm
    • 1
  • Hardi Hungar
    • 1
  • Peter Jansen
    • 3
  1. 1.Carl von Ossietzky UniversitatHeerstrafβeGermany
  2. 2.OFFISOldenburgGermany
  3. 3.BMW AGMunichGermany

Personalised recommendations