Challenges in the Verification of Electronic Control Units

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 (http://www.informatik.uni-oldenburg.de/leute/damm.html) and Offis (http://www.offis.de/indexe.htm)