You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at
  • technical reports and other articles issued by Mälardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact

Challenges in the Verification of Electronic Control Units


Prof. Werner Damm



Start time:

2000-12-07 14:00

End time:

2000-12-07 15:00


Vargens Vret room V222

Contact person:


Electronic Control Units control our cars, airplanes, trains, and other safety critical systems. The key motivation to maintain high safety standards in the light of increasing complexity as well as the need to reduce development costs, in particular time spent in testing, have been driving forces in promoting the use of formal techniques in software requirement specifications as well as during design and validation of software. As a result of this drive and the growing maturity of the employed verification tools, formal techniques have found their way into industrial design flows, such as the use of the B-method in Matra- Transport, and the use of the Sternol Verification Environment based on Prover at Adtranz Signaling Sweden. We see an increased pressure on the design process for on-board control software to move towards a formally based process, a central prerequisite being the introduction of a model-based development process. This in itself constitutes already a significant shift. The step to model-based design processes has to a somewhat larger extent already been taken in both avionics and automotive, where tools like STATEMATE, Mathworks, MatrixX, Scade, ASCET are routinely used at different stages in the development process for control software. E.g. Aerospatial uses the Scade tool to generate airborne software and the induced cost benefits. The same concern about safety has caused companies like Boeing and British Aerospace to also asses the use of formal verification methods. Similarly, in automotive, the incentive to reduce development costs by letting model-checking catch errors early on in the development process, or the use of model-checking to create a golden reference model in the manufacturer-supplier chain, has been a major motivation to investigate the use of model-checking based verification techniques.The talk surveys the state of the art in employing verification techniques in the above application domains, stressing the role of such techniques in a model based design process. The technical focus of the talk will be on recent advances in model-checking, allowing to integrate a limited degree of first-order reasoning into symbolic model-checking. The talk will also present evaluation results on using SAT based methods in connection with bounded model checking on representative industrial designs.Prof. Werner Damm is at Uni Oldenburg ( and Offis (