This paper describes the applications of model-checking based verification tools to specification models of automative 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 extentions 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.
['Tom Bienmüller', 'Jürgen Bohn', 'Henning Brinkmann', 'Udo Brockmeyer', 'Werner Damm', 'Hardi Hungar', 'Peter Jansen']
Verification of Automotive Control Units